From 1dad28af797b80ac6f8cd66c0bbd6422e59d12ec Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 18 Nov 2019 13:33:47 -0800
Subject: [PATCH] chore: remove temp hack

---
 library/Init/Lean/Name.lean | 2 --
 1 file changed, 2 deletions(-)

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⟩