diff --git a/library/Init/Lean/Name.lean b/library/Init/Lean/Name.lean
index e0f8603944..3ddb97a180 100644
--- a/library/Init/Lean/Name.lean
+++ b/library/Init/Lean/Name.lean
@@ -21,8 +21,6 @@ inductive Name
 attribute [extern "lean_name_mk_string"] Name.str
 attribute [extern "lean_name_mk_numeral"] Name.num
 
-@[matchPattern] abbrev Name.mkString := Name.str
-
 instance : Inhabited Name :=
 ⟨Name.anonymous⟩