diff --git a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
index d042a474f1..b0d50b86f7 100644
--- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
@@ -671,6 +671,7 @@ where
 
 @[builtinDelab app.namedPattern]
 def delabNamedPattern : Delab := do
+  guard (← read).inPattern
   guard $ (← getExpr).getAppNumArgs == 3
   let x ← withAppFn $ withAppArg delab
   let p ← withAppArg delab
diff --git a/tests/lean/run/PPTopDownAnalyze.lean b/tests/lean/run/PPTopDownAnalyze.lean
index 339fce4036..6633f55113 100644
--- a/tests/lean/run/PPTopDownAnalyze.lean
+++ b/tests/lean/run/PPTopDownAnalyze.lean
@@ -227,6 +227,7 @@ def fooReadGetModify : ReaderT Unit (StateT Unit IO) Unit := do
 #testDelabN MonadLift.noConfusionType
 #testDelabN MonadExcept.noConfusion
 #testDelabN MonadFinally.noConfusion
+#testDelabN Lean.Elab.InfoTree.goalsAt?.match_1
 
 -- TODO: this test is broken because of the inability to solve structural max constraints
 -- (See https://github.com/leanprover/lean4/issues/590)
@@ -237,6 +238,3 @@ def fooReadGetModify : ReaderT Unit (StateT Unit IO) Unit := do
 -- TODO: this is broken because it is currently inaccessible names
 -- #testDelabN Std.ShareCommon.ObjectMap.find?
 -- #testDelabN Std.ShareCommon.ObjectMap.insert
-
--- TODO: these fail because we are not disable named patterns when not using `match` syntax
--- #testDelabN Lean.Elab.InfoTree.goalsAt?.match_1