From 9ee1ff243528a377243fb2434b2a410a9355eb3b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Wed, 13 Mar 2024 20:46:04 -0700
Subject: [PATCH] chore: remove bootstrapping workaround

---
 src/Lean/Elab/Declaration.lean | 1 -
 src/Lean/Elab/DefView.lean     | 3 ---
 src/Lean/Parser/Command.lean   | 4 +---
 3 files changed, 1 insertion(+), 7 deletions(-)

diff --git a/src/Lean/Elab/Declaration.lean b/src/Lean/Elab/Declaration.lean
index 90e2cf682b..70ea51f354 100644
--- a/src/Lean/Elab/Declaration.lean
+++ b/src/Lean/Elab/Declaration.lean
@@ -43,7 +43,6 @@ private def isNamedDef (stx : Syntax) : Bool :=
     let k := decl.getKind
     k == ``Lean.Parser.Command.abbrev ||
     k == ``Lean.Parser.Command.definition ||
-    k == ``Lean.Parser.Command.def || -- TODO: delete
     k == ``Lean.Parser.Command.theorem ||
     k == ``Lean.Parser.Command.opaque ||
     k == ``Lean.Parser.Command.axiom ||
diff --git a/src/Lean/Elab/DefView.lean b/src/Lean/Elab/DefView.lean
index 71c1f92429..1ac40b2bfd 100644
--- a/src/Lean/Elab/DefView.lean
+++ b/src/Lean/Elab/DefView.lean
@@ -143,7 +143,6 @@ def isDefLike (stx : Syntax) : Bool :=
   let declKind := stx.getKind
   declKind == ``Parser.Command.abbrev ||
   declKind == ``Parser.Command.definition ||
-  declKind == ``Parser.Command.def || -- TODO: delete
   declKind == ``Parser.Command.theorem ||
   declKind == ``Parser.Command.opaque ||
   declKind == ``Parser.Command.instance ||
@@ -155,8 +154,6 @@ def mkDefView (modifiers : Modifiers) (stx : Syntax) : CommandElabM DefView :=
     return mkDefViewOfAbbrev modifiers stx
   else if declKind == ``Parser.Command.definition then
     return mkDefViewOfDef modifiers stx
-  else if declKind == ``Parser.Command.def then -- TODO: delete
-    return mkDefViewOfDef modifiers stx
   else if declKind == ``Parser.Command.theorem then
     return mkDefViewOfTheorem modifiers stx
   else if declKind == ``Parser.Command.opaque then
diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean
index 995d55d43f..1035dc9aad 100644
--- a/src/Lean/Parser/Command.lean
+++ b/src/Lean/Parser/Command.lean
@@ -116,8 +116,6 @@ def optDefDeriving   :=
   optional (ppDedent ppLine >> atomic ("deriving " >> notSymbol "instance") >> sepBy1 ident ", ")
 def definition     := leading_parser
   "def " >> recover declId skipUntilWsOrDelim >> ppIndent optDeclSig >> declVal >> optDefDeriving
-def «def»     := leading_parser -- TODO: delete
-  "def " >> recover declId skipUntilWsOrDelim >> ppIndent optDeclSig >> declVal >> optDefDeriving
 def «theorem»        := leading_parser
   "theorem " >> recover declId skipUntilWsOrDelim >> ppIndent declSig >> declVal
 def «opaque»         := leading_parser
@@ -200,7 +198,7 @@ def «structure»          := leading_parser
     optDeriving
 @[builtin_command_parser] def declaration := leading_parser
   declModifiers false >>
-  («abbrev» <|> definition <|> «def» <|> «theorem» <|> «opaque» <|> «instance» <|> «axiom» <|> «example» <|>
+  («abbrev» <|> definition <|> «theorem» <|> «opaque» <|> «instance» <|> «axiom» <|> «example» <|>
    «inductive» <|> classInductive <|> «structure»)
 @[builtin_command_parser] def «deriving»     := leading_parser
   "deriving " >> "instance " >> derivingClasses >> " for " >> sepBy1 (recover ident skip) ", "