diff --git a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
index 365d2bd691..ca2b3ced56 100644
--- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
@@ -576,7 +576,7 @@ partial def delabDoElems : DelabM (List Syntax) := do
             prependAndRec `(doElem|let $n:term ← $ma)
           else
             prependAndRec `(doElem|$ma:term)
-      | _ => delabAndRet
+      | _ => failure
   else if e.isLet then
     let Expr.letE n t v b _ ← getExpr | unreachable!
     let n ← getUnusedName n b
@@ -587,10 +587,10 @@ partial def delabDoElems : DelabM (List Syntax) := do
       descend b 2 $
         prependAndRec `(doElem|let $(mkIdent n) : $stxT := $stxV)
   else
-    delabAndRet
+    let stx ← delab
+    [←`(doElem|$stx:term)]
   where
     prependAndRec x : DelabM _ := List.cons <$> x <*> delabDoElems
-    delabAndRet : DelabM _ := do let stx ← delab; [←`(doElem|$stx:term)]
 
 @[builtinDelab app.Bind.bind]
 def delabDo : Delab := whenPPOption getPPNotation do
diff --git a/tests/lean/PPRoundtrip.lean b/tests/lean/PPRoundtrip.lean
index 94ad4fefb7..5062229bbc 100644
--- a/tests/lean/PPRoundtrip.lean
+++ b/tests/lean/PPRoundtrip.lean
@@ -100,3 +100,5 @@ set_option pp.structure_instance_type true in
   discard <| pure 2
   let y := 3
   return x + y))
+
+#eval checkM `(typeAs (Id Nat) (pure 1 >>= pure))
diff --git a/tests/lean/PPRoundtrip.lean.expected.out b/tests/lean/PPRoundtrip.lean.expected.out
index ccb3dbf9ec..13998ab219 100644
--- a/tests/lean/PPRoundtrip.lean.expected.out
+++ b/tests/lean/PPRoundtrip.lean.expected.out
@@ -63,3 +63,5 @@ typeAs Nat
     discard (pure 2)
     let y : Nat := 3
     pure (x + y))
+typeAs (Id Nat)
+  (pure 1 >>= pure)