@@ -138,7 +138,7 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot hints ist
139 -- if all else fails, make a new metavariable
139 -- if all else fails, make a new metavariable
140 (if fromProver
140 (if fromProver
141− then cantSolveGoal
141+ then fail "cantSolveGoal"
142 else do attack; defer [] nroot; solve) True) True
142 else do attack; defer [] nroot; solve) True) True
144 getFn d Nothing = []
144 getFn d Nothing = []