diff --git a/tests/atomic.ref b/tests/atomic.ref
index 7146b97eacba07167809160248fe52f86fe6892d..ba5c5ad608616ab2992086c7e9411483ad6fe03e 100644
--- a/tests/atomic.ref
+++ b/tests/atomic.ref
@@ -17,10 +17,7 @@
 The command has indeed failed with message:
 Tactic failure: iAuIntro: not all spatial assumptions are laterable.
 The command has indeed failed with message:
-Tactic failure: wp_apply: cannot apply
-(<<< ∀ (v : val) (q : Qp), ?Goal ↦{q} v >>>
-   ! #?Goal @ ⊤
- <<< ?Goal ↦{q} v, RET v >>>).
+Tactic failure: iAuIntro: not all spatial assumptions are laterable.
 "printing"
      : string
 1 subgoal
diff --git a/tests/atomic.v b/tests/atomic.v
index 4e69316d0a7253ce02964cf5cb19033b59a4e9e6..125a261c18bfaa41ae9246fa617025aa02104174 100644
--- a/tests/atomic.v
+++ b/tests/atomic.v
@@ -30,7 +30,7 @@ Section error.
   Restart.
     iIntros "HP". Fail awp_apply load_spec.
   Abort.
-End error.  
+End error.
 
 
 (* Test if AWP and the AU obtained from AWP print. *)
diff --git a/theories/heap_lang/proofmode.v b/theories/heap_lang/proofmode.v
index fc4913c1bcc81d016f23c6e229bbc7a19cbdfc55..95ae906c193c924994399d273968507f390feb54 100644
--- a/theories/heap_lang/proofmode.v
+++ b/theories/heap_lang/proofmode.v
@@ -435,9 +435,11 @@ the context, which is intended to be the non-laterable assertions that iAuIntro
 would choke on.  You get them all back in the continuation of the atomic
 operation. *)
 Tactic Notation "awp_apply" open_constr(lem) :=
-  wp_apply_core lem (fun H => iApplyHyp H; last iAuIntro).
+  (wp_apply_core lem (fun H => iApplyHyp H));
+  last iAuIntro.
 Tactic Notation "awp_apply" open_constr(lem) "without" constr(Hs) :=
-  wp_apply_core lem (fun H => iApply wp_frame_wand_l; iSplitL Hs; [iAccu|iApplyHyp H; last iAuIntro]).
+  (wp_apply_core lem (fun H => iApply wp_frame_wand_l; iSplitL Hs; [iAccu|iApplyHyp H]));
+  last iAuIntro.
 
 Tactic Notation "wp_alloc" ident(l) "as" constr(H) :=
   let Htmp := iFresh in