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