diff --git a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
index 52350a98c4..50f83ed2e8 100644
--- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
@@ -671,11 +671,9 @@ def delabStructureInstance : Delab := do
         paramMap := paramMap.insert (← x.fvarId!.getUserName) param
       return paramMap
     let (_, fields) ← collectStructFields s.induct paramMap #[] {} s
-    if ← withType <| getPPOption getPPStructureInstanceType then
-      let tyStx ← withType delab
-      `({ $fields,* : $tyStx })
-    else
-      `({ $fields,* })
+    let tyStx? : Option Term ← withType do
+      if ← getPPOption getPPStructureInstanceType then delab else pure none
+    `({ $fields,* $[: $tyStx?]? })
 
 
 /-- State for `delabAppMatch` and helpers. -/