@@ -337,12 +337,13 @@ makeLemma fn updatefile l n
337337
338338 if (not isProv) then do
339339 let skip = guessImps i (tt_ctxt i) mty
340− let classes = guessClasses i (tt_ctxt i) mty
340+ let impty = stripMNBind skip margs (delab i mty)
341+ let classes = guessClasses i (tt_ctxt i) [] (allNamesIn impty) mty
341342
342343 let lem = show n ++ " : " ++
343344 constraints i classes mty ++
344345 showTmOpts (defaultPPOption { ppopt_pinames = True })
345− (stripMNBind skip margs (delab i mty))
346+ impty
346347 let lem_app = guessBrackets False tyline (show n) (show n ++ appArgs skip margs mty)
347348
348349 if updatefile then
@@ -385,13 +386,20 @@ makeLemma fn updatefile l n
385386 appArgs skip i (Bind _ (Pi _ _ _) sc) = appArgs skip (i - 1) sc
386387 appArgs skip i _ = ""
387388
388− stripMNBind _ args t | args <= 0 = t
389+ stripMNBind _ args t | args <= 0 = stripImp t
389390 stripMNBind skip args (PPi b n@(UN c) _ ty sc)
390391 | n `notElem` skip ||
391392 take 4 (str c) == "__pi" -- keep in type, but not in app
392− = PPi b n NoFC ty (stripMNBind skip (args - 1) sc)
393+ = PPi b n NoFC (stripImp ty) (stripMNBind skip (args - 1) sc)
393394 stripMNBind skip args (PPi b _ _ ty sc) = stripMNBind skip (args - 1) sc
394− stripMNBind skip args t = t
395+ stripMNBind skip args t = stripImp t
396+
397+ stripImp (PApp fc f as) = PApp fc (stripImp f) (map placeholderImp as)
398+ where
399+ placeholderImp tm@(PImp _ _ _ _ _) = tm { getTm = Placeholder }
400+ placeholderImp tm = tm { getTm = stripImp (getTm tm) }
401+ stripImp (PPi b n f ty sc) = PPi b n f (stripImp ty) (stripImp sc)
402+ stripImp t = t
395403
396404 constraints :: IState -> [Name] -> Type -> String
397405 constraints i [] ty = ""
@@ -431,12 +439,19 @@ makeLemma fn updatefile l n
431439 "_aX" -> True
432440 _ -> False
433441
434− guessClasses :: IState -> Context -> Term -> [Name]
435− guessClasses ist ctxt (Bind n (Pi _ ty _) sc)
436− | isParamClass ist ty
437− = n : guessClasses ist ctxt sc
438− | otherwise = guessClasses ist ctxt sc
439− guessClasses ist ctxt _ = []
442+ guessClasses :: IState -> Context -> [Name] -> [Name] -> Term -> [Name]
443+ guessClasses ist ctxt binders usednames (Bind n (Pi _ ty _) sc)
444+ | isParamClass ist ty && any (\x -> elem x usednames)
445+ (paramNames binders ty)
446+ = n : guessClasses ist ctxt (n : binders) usednames sc
447+ | otherwise = guessClasses ist ctxt (n : binders) usednames sc
448+ guessClasses ist ctxt _ _ _ = []
449+
450+ paramNames bs ty | (P _ _ _, args) <- unApply ty
451+ = vnames args
452+ where vnames [] = []
453+ vnames (V i : xs) | i < length bs = bs !! i : vnames xs
454+ vnames (_ : xs) = vnames xs
440455
441456 isClass ist t
442457 | (P _ n _, args) <- unApply t