diff --git a/theories/heap_lang/proofmode.v b/theories/heap_lang/proofmode.v
index 98ea0e6758ebc15bcc7577466f5034ad664f91ba..cb9c1a2afbd6c7d4dc53cc9d3de4dfb3fa557c33 100644
--- a/theories/heap_lang/proofmode.v
+++ b/theories/heap_lang/proofmode.v
@@ -97,7 +97,7 @@ Tactic Notation "wp_pure" open_constr(efoc) :=
       unify e' efoc;
       eapply (tac_twp_pure _ _ _ (fill K e'));
       [iSolveTC                       (* PureExec *)
-      |try fast_done                  (* The pure condition for PureExec *)
+      |try solve_vals_compare_safe    (* The pure condition for PureExec *)
       |wp_finish                      (* new goal *)
       ])
     || fail "wp_pure: cannot find" efoc "in" e "or" efoc "is not a redex"