@@ -407,7 +407,8 @@ letbind n ty val ctxt env _ = fail "Can't let bind here"
407rewrite :: Raw -> RunTactic
407rewrite :: Raw -> RunTactic
408rewrite tm ctxt env (Bind x (Hole t) xp@(P _ x' _)) | x == x' =
408rewrite tm ctxt env (Bind x (Hole t) xp@(P _ x' _)) | x == x' =
409 do (tmv, tmt) <- lift $ check ctxt env tm
409 do (tmv, tmt) <- lift $ check ctxt env tm
410+ let tmt' = normalise ctxt env tmt
410− case unApply tmt of
411+ case unApply tmt' of
411 (P _ (UN "=") _, [lt,rt,l,r]) ->
412 (P _ (UN "=") _, [lt,rt,l,r]) ->
412 do let p = Bind rname (Lam lt) (mkP (P Bound rname lt) r l t)
413 do let p = Bind rname (Lam lt) (mkP (P Bound rname lt) r l t)
413 let newt = mkP l r l t
414 let newt = mkP l r l t