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