From 6cbfe2359bb182ea92963a8f757c1522b1706111 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Wed, 19 Aug 2020 13:21:51 +0200
Subject: [PATCH] chore: remove old syntax

---
 src/Lean/Parser/Level.lean |  4 ++--
 src/Lean/Parser/Term.lean  | 11 ++++-------
 2 files changed, 6 insertions(+), 9 deletions(-)

diff --git a/src/Lean/Parser/Level.lean b/src/Lean/Parser/Level.lean
index 5c83d32074..db827c1232 100644
--- a/src/Lean/Parser/Level.lean
+++ b/src/Lean/Parser/Level.lean
@@ -21,8 +21,8 @@ namespace Level
 @[builtinLevelParser] def max    := parser! nonReservedSymbol "max " true  >> many1 (levelParser maxPrec)
 @[builtinLevelParser] def imax   := parser! nonReservedSymbol "imax " true >> many1 (levelParser maxPrec)
 @[builtinLevelParser] def hole   := parser! "_"
-@[builtinLevelParser] def num    := checkInsideQuot >> numLit <|> checkOutsideQuot >> parser! numLit
-@[builtinLevelParser] def ident  := checkInsideQuot >> ident <|> checkOutsideQuot >> parser! ident
+@[builtinLevelParser] def num    := numLit
+@[builtinLevelParser] def ident  := ident
 @[builtinLevelParser] def addLit := tparser!:65 "+" >> numLit
 
 end Level
diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean
index 4f8c446d0b..b8fd64960e 100644
--- a/src/Lean/Parser/Term.lean
+++ b/src/Lean/Parser/Term.lean
@@ -43,13 +43,10 @@ checkPrec prec >> symbol sym >> termParser (prec+1)
 def leadPrec := maxPrec - 1
 
 /- Built-in parsers -/
-def explicitUniv' := checkNoWsBefore "no space before '.{'" >> parser! ".{" >> sepBy1 levelParser ", " >> "}"
-def namedPattern' := checkNoWsBefore "no space before '@'" >> parser! "@" >> termParser maxPrec
-@[builtinTermParser] def id := checkOutsideQuot >> parser! ident >> optional (explicitUniv' <|> namedPattern')
-@[builtinTermParser] def ident := checkInsideQuot >> Parser.ident
-@[builtinTermParser] def num : Parser := checkInsideQuot >> numLit <|> checkOutsideQuot >> parser! numLit
-@[builtinTermParser] def str : Parser := checkInsideQuot >> strLit <|> checkOutsideQuot >> parser! strLit
-@[builtinTermParser] def char : Parser := checkInsideQuot >> charLit <|> checkOutsideQuot >> parser! charLit
+@[builtinTermParser] def ident := Parser.ident
+@[builtinTermParser] def num : Parser := numLit
+@[builtinTermParser] def str : Parser := strLit
+@[builtinTermParser] def char : Parser := charLit
 @[builtinTermParser] def type := parser! "Type" >> optional (checkWsBefore "" >> checkPrec (maxPrec-1) >> levelParser maxPrec)
 @[builtinTermParser] def sort := parser! "Sort" >> optional (checkWsBefore "" >> checkPrec (maxPrec-1) >> levelParser maxPrec)
 @[builtinTermParser] def prop := parser! "Prop"