@@ -238,14 +238,18 @@ goalAtFocus ps
238238
239239goal :: Hole -> Term -> TC Goal
240240goal h tm = g [] tm where
241+ g env (Bind n b@(Guess _ _) sc)
242+ | same h n = return $ GD env b
243+ | otherwise
244+ = gb env b `mplus` g ((n, b):env) sc
241245 g env (Bind n b sc) | hole b && same h n = return $ GD env b
242246 | otherwise
243− = gb env b `mplus` g ((n, b):env) sc
247+ = g ((n, b):env) sc `mplus` gb env b
244248 g env (App f a) = g env f `mplus` g env a
245249 g env t = fail "Can't find hole"
246250
247− gb env (Let t v) = g env t `mplus` g env v
248− gb env (Guess t v) = g env t `mplus` g env v
251+ gb env (Let t v) = g env v `mplus` g env t
252+ gb env (Guess t v) = g env v `mplus` g env t
249253 gb env t = g env (binderTy t)
250254
251255tactic :: Hole -> RunTactic -> StateT TState TC ()