@@ -238,14 +238,18 @@ goalAtFocus ps
239goal :: Hole -> Term -> TC Goal
239goal :: Hole -> Term -> TC Goal
240goal h tm = g [] tm where
240goal h tm = g [] tm where
241+ g env (Bind n b@(Guess _ _) sc)
242+ | same h n = return $ GD env b
244+ = gb env b `mplus` g ((n, b):env) sc
241 g env (Bind n b sc) | hole b && same h n = return $ GD env b
245 g env (Bind n b sc) | hole b && same h n = return $ GD env b
242 | otherwise
246 | otherwise
243− = gb env b `mplus` g ((n, b):env) sc
247+ = g ((n, b):env) sc `mplus` gb env b
244 g env (App f a) = g env f `mplus` g env a
248 g env (App f a) = g env f `mplus` g env a
245 g env t = fail "Can't find hole"
249 g env t = fail "Can't find hole"
247− gb env (Let t v) = g env t `mplus` g env v
251+ gb env (Let t v) = g env v `mplus` g env t
248− gb env (Guess t v) = g env t `mplus` g env v
252+ gb env (Guess t v) = g env v `mplus` g env t
249 gb env t = g env (binderTy t)
253 gb env t = g env (binderTy t)
251tactic :: Hole -> RunTactic -> StateT TState TC ()
255tactic :: Hole -> RunTactic -> StateT TState TC ()