diff --git a/iris_heap_lang/proofmode.v b/iris_heap_lang/proofmode.v
index 7c048fcf5093e6a0620da164f730f229668ed666..4d72ae4faec7bcb0a48eba05296bcc8674fd06ac 100644
--- a/iris_heap_lang/proofmode.v
+++ b/iris_heap_lang/proofmode.v
@@ -727,7 +727,8 @@ premise. The second one additionaly does some framing: it gets rid of [Hs] from
 the context, reducing clutter. You get them all back in the continuation of the
 atomic operation. *)
 Tactic Notation "awp_apply" open_constr(lem) :=
-  wp_apply_core lem ltac:(fun H => iApplyHyp H) ltac:(fun cont => fail);
+  (* [pm_prettify] is needed to clean up telescopes. *)
+  wp_apply_core lem ltac:(fun H => iApplyHyp H; pm_prettify) ltac:(fun cont => fail);
   last iAuIntro.
 Tactic Notation "awp_apply" open_constr(lem) "without" constr(Hs) :=
   (* Convert "list of hypothesis" into specialization pattern. *)
@@ -736,7 +737,8 @@ Tactic Notation "awp_apply" open_constr(lem) "without" constr(Hs) :=
   wp_apply_core lem
     ltac:(fun H =>
       iApply (wp_frame_wand with
-        [SGoal $ SpecGoal GSpatial false [] Hs false]); [iAccu|iApplyHyp H])
+        [SGoal $ SpecGoal GSpatial false [] Hs false]);
+         [iAccu|iApplyHyp H; pm_prettify])
     ltac:(fun cont => fail);
   last iAuIntro.
 
diff --git a/tests/atomic.ref b/tests/atomic.ref
index 90a359e12dfccdd617576282f4644185eed71eef..131326ff04952758910caff13aea245513a9dff2 100644
--- a/tests/atomic.ref
+++ b/tests/atomic.ref
@@ -1,3 +1,22 @@
+"test_awp_apply"
+     : string
+1 goal
+  
+  Σ : gFunctors
+  heapGS0 : heapGS Σ
+  aheap : atomic_heap
+  Q : iProp Σ
+  l : loc
+  v : val
+  ============================
+  "HQ" : Q
+  "Hl" : l ↦ v
+  --------------------------------------∗
+  AACC << ∃∃ (v0 : val) (q : dfrac), l ↦{q} v0, ABORT Q ∗ l ↦ v >>
+       @ ⊤ ∖ ∅, ∅
+       << l ↦{q} v0, COMM Q >>
+"test_awp_apply_without"
+     : string
 1 goal
   
   H : atomic_heap
@@ -10,9 +29,9 @@
   ============================
   "Hl" : l ↦ v
   --------------------------------------∗
-  atomic_acc (⊤ ∖ ∅) ∅ (tele_app (λ (v0 : val) (q : dfrac), l ↦{q} v0))
-    (l ↦ v) (tele_app (λ (v0 : val) (q : dfrac), tele_app (l ↦{q} v0)))
-    (λ.. (_ : [tele (_ : val) (_ : dfrac)]) (_ : [tele]), Q -∗ Q)
+  AACC << ∃∃ (v0 : val) (q : dfrac), l ↦{q} v0, ABORT l ↦ v >>
+       @ ⊤ ∖ ∅, ∅
+       << l ↦{q} v0, COMM Q -∗ Q >>
 "printing"
      : string
 1 goal
diff --git a/tests/atomic.v b/tests/atomic.v
index 32b5595bca4177690914c8c607b8ce369aac7615..26688dbf229b81103aeb6c9ef51e48893498ab5a 100644
--- a/tests/atomic.v
+++ b/tests/atomic.v
@@ -25,7 +25,15 @@ Section tests.
   Context `{!atomic_heap, !heapGS Σ, !atomic_heapGS Σ}.
   Import atomic_heap.notation.
 
-  (* FIXME: removing the `val` type annotation breaks printing. *)
+  Check "test_awp_apply".
+  Lemma test_awp_apply (Q : iProp Σ) (l : loc) v :
+    Q -∗ l ↦ v -∗ WP !#l {{ _, Q }}.
+  Proof.
+    iIntros "HQ Hl". awp_apply load_spec. Show.
+    iAaccIntro with "Hl"; eauto with iFrame.
+  Qed.
+
+  Check "test_awp_apply_without".
   Lemma test_awp_apply_without (Q : iProp Σ) (l : loc) v :
     Q -∗ l ↦ v -∗ WP !#l {{ _, Q }}.
   Proof.