diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index cbe06624fe..e9038f79f1 100644
--- a/src/Init/Prelude.lean
+++ b/src/Init/Prelude.lean
@@ -170,9 +170,6 @@ structure Subtype {α : Sort u} (p : α → Prop) where
 /-- Auxiliary Declaration used to implement the notation (a : α) -/
 @[reducible] def typedExpr (α : Sort u) (a : α) : α := a
 
--- TODO: delete
-@[reducible] def namedPatternOld {α : Sort u} (x a : α) : α := a
-
 /-- Auxiliary Declaration used to implement the named patterns `x@h:p` -/
 @[reducible] def namedPattern {α : Sort u} (x a : α) (h : Eq x a) : α := a
 
diff --git a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
index 3b0e7a74cf..6df1bbb724 100644
--- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
@@ -685,16 +685,6 @@ where
       | none   => withBindingBodyUnusedName fun h => do
         return (← delab, h.getId)
 
-@[builtinDelab app.namedPatternOld]
-def delabNamedPatternOld : Delab := do
-  -- Note: we keep this as a delaborator because it accesses the DelabM context
-  guard (← read).inPattern
-  guard $ (← getExpr).getAppNumArgs == 3
-  let x ← withAppFn $ withAppArg delab
-  let p ← withAppArg delab
-  guard x.isIdent
-  `($x:ident@$p:term)
-
 @[builtinDelab app.namedPattern]
 def delabNamedPattern : Delab := do
   -- Note: we keep this as a delaborator because it accesses the DelabM context