@@ -759,9 +759,13 @@ try' t1 t2 proofSearch
759 = do s <- get
759 = do s <- get
760 ps <- get_probs
760 ps <- get_probs
761 ulog <- getUnifyLog
761 ulog <- getUnifyLog
762+ ivs <- get_instances
762 case prunStateT 999999 False ps t1 s of
763 case prunStateT 999999 False ps t1 s of
763− OK ((v, _, _), s') -> do put s'
764+ OK ((v, _, _), s')
765+ | length (instances (proof s')) <= length ivs ->
764 return $! v
767 return $! v
765 Error e1 -> traceWhen ulog ("try failed " ++ show e1) $
769 Error e1 -> traceWhen ulog ("try failed " ++ show e1) $
766 if recoverableErr e1 then
770 if recoverableErr e1 then
767 do case runStateT t2 s of
771 do case runStateT t2 s of