@@ -168,9 +168,11 @@ updateSolved xs pt@(PT path env sub)
168168 (updateSolvedTerm xs sub)
169169
170170goal :: Hole -> ProofTerm -> TC Goal
171−goal h pt@(PT path env sub) = do let tm = rebuildTerm sub path
172− ginf <- g [] (rebuildTerm sub path)
173− return ginf where
171+goal h pt@(PT path env sub)
172+ | OK ginf <- g env sub = return ginf
173+ | otherwise = g [] (rebuildTerm sub path)
174+ where
175+ g :: Env -> Term -> TC Goal
174176 g env (Bind n b@(Guess _ _) sc)
175177 | same h n = return $ GD env b
176178 | otherwise