@@ -370,7 +370,8 @@ elab ist info emode opts fn tm
370370 elabE (True, a, True, qq) sc
371371 solve
372372 elab' ina@(_, a, inty, qq) (PLet n ty val sc)
373− = do attack;
373+ = do attack
374+ ivs <- get_instances
374375 tyn <- getNameFrom (sMN 0 "letty")
375376 claim tyn RType
376377 valn <- getNameFrom (sMN 0 "letval")
@@ -384,6 +385,17 @@ elab ist info emode opts fn tm
384385 elabE (True, a, True, qq) ty
385386 focus valn
386387 elabE (True, a, True, qq) val
388+ ivs' <- get_instances
389+ when (not pattern) $
390+ mapM_ (\n -> do focus n
391+ g <- goal
392+ hs <- get_holes
393+ if all (\n -> n == tyn || not (n `elem` hs)) (freeNames g)
394+ -- let insts = filter tcname $ map fst (ctxtAlist (tt_ctxt ist))
395+ then try (resolveTC 7 g fn ist)
396+ (movelast n)
397+ else movelast n)
398+ (ivs' \\ ivs)
387399 env <- get_env
388400 elabE (True, a, inty, qq) sc
389401 -- HACK: If the name leaks into its type, it may leak out of