diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean
index d636427401..5a4bcd658a 100644
--- a/src/Lean/Parser/Command.lean
+++ b/src/Lean/Parser/Command.lean
@@ -54,15 +54,15 @@ def «constant»       := parser! "constant " >> declId >> declSig >> optional d
 def «instance»       := parser! "instance " >> optional declId >> declSig >> declVal
 def «axiom»          := parser! "axiom " >> declId >> declSig
 def «example»        := parser! "example " >> declSig >> declVal
-def inferMod         := parser! try ("{" >> "}")
+def inferMod         := parser! try (symbol "{" appPrec >> "}")
 def introRule        := parser! " | " >> ident >> optional inferMod >> optDeclSig
 def «inductive»      := parser! "inductive " >> declId >> optDeclSig >> many introRule
 def classInductive   := parser! try ("class " >> "inductive ") >> declId >> optDeclSig >> many introRule
-def structExplicitBinder := parser! "(" >> many ident >> optional inferMod >> optDeclSig >> optional Term.binderDefault >> ")"
-def structImplicitBinder := parser! "{" >> many ident >> optional inferMod >> optDeclSig >> "}"
-def structInstBinder     := parser! "[" >> many ident >> optional inferMod >> optDeclSig >> "]"
+def structExplicitBinder := parser! symbol "(" appPrec >> many ident >> optional inferMod >> optDeclSig >> optional Term.binderDefault >> ")"
+def structImplicitBinder := parser! symbol "{" appPrec >> many ident >> optional inferMod >> optDeclSig >> "}"
+def structInstBinder     := parser! symbol "[" appPrec >> many ident >> optional inferMod >> optDeclSig >> "]"
 def structFields         := parser! many (structExplicitBinder <|> structImplicitBinder <|> structInstBinder)
-def structCtor           := parser! ident >> optional inferMod >> " :: "
+def structCtor           := parser! ident >> optional inferMod >> symbol " :: " 67
 def structureTk          := parser! "structure "
 def classTk              := parser! "class "
 def «extends»            := parser! " extends " >> sepBy1 termParser ", "
@@ -85,12 +85,12 @@ declModifiers >> («abbrev» <|> «def» <|> «theorem» <|> «constant» <|> «
 @[builtinCommandParser] def «resolve_name» := parser! "#resolve_name " >> ident
 @[builtinCommandParser] def «init_quot»    := parser! "init_quot"
 @[builtinCommandParser] def «set_option»   := parser! "set_option " >> ident >> (nonReservedSymbol "true" <|> nonReservedSymbol "false" <|> strLit <|> numLit)
-@[builtinCommandParser] def «attribute»    := parser! optional "local " >> "attribute " >> "[" >> sepBy1 attrInstance ", " >> "]" >> many1 ident
-@[builtinCommandParser] def «export»       := parser! "export " >> ident >> "(" >> many1 ident >> ")"
+@[builtinCommandParser] def «attribute»    := parser! optional "local " >> "attribute " >> symbol "[" appPrec >> sepBy1 attrInstance ", " >> "]" >> many1 ident
+@[builtinCommandParser] def «export»       := parser! "export " >> ident >> symbol "(" appPrec >> many1 ident >> ")"
 def openHiding       := parser! try (ident >> "hiding") >> many1 ident
 def openRenamingItem := parser! ident >> unicodeSymbol "→" "->" >> ident
 def openRenaming     := parser! try (ident >> "renaming") >> sepBy1 openRenamingItem ", "
-def openOnly         := parser! try (ident >> "(") >> many1 ident >> ")"
+def openOnly         := parser! try (ident >> symbol "(" appPrec) >> many1 ident >> ")"
 def openSimple       := parser! many1 ident
 @[builtinCommandParser] def «open»    := parser! "open " >> (openHiding <|> openRenaming <|> openOnly <|> openSimple)
 
diff --git a/src/Lean/Parser/Parser.lean b/src/Lean/Parser/Parser.lean
index ab53fd5f71..17a01d28c2 100644
--- a/src/Lean/Parser/Parser.lean
+++ b/src/Lean/Parser/Parser.lean
@@ -1153,7 +1153,7 @@ def unquotedSymbol : Parser :=
 { fn := unquotedSymbolFn }
 
 instance stringToParserCoe : HasCoe String Parser :=
-⟨symbolAux⟩
+⟨fun s => symbol s 0⟩
 
 namespace ParserState
 
@@ -1423,7 +1423,7 @@ def pushNone : Parser :=
 { fn := fun c s => s.pushSyntax mkNullNode }
 
 -- We support two kinds of antiquotations: `$id` and `$(t)`, where `id` is a term identifier and `t` is a term.
-def antiquotNestedExpr : Parser := node `antiquotNestedExpr ("(" >> termParser >> ")")
+def antiquotNestedExpr : Parser := node `antiquotNestedExpr (symbol "(" appPrec >> termParser >> ")")
 def antiquotExpr : Parser       := identNoAntiquot <|> antiquotNestedExpr
 
 /--
@@ -1444,7 +1444,7 @@ node kind $ try $
   many (checkNoWsBefore "" >> dollarSymbol) >>
   checkNoWsBefore "no space before spliced term" >> antiquotExpr >>
   nameP >>
-  optional (checkNoWsBefore "" >> "*")
+  optional (checkNoWsBefore "" >> symbolAux "*" none)
 
 def tryAnti (c : ParserContext) (s : ParserState) : Bool :=
 let (s, stx?) := peekToken c s;
diff --git a/src/Lean/Parser/Syntax.lean b/src/Lean/Parser/Syntax.lean
index aa16e738b1..04a8d5082b 100644
--- a/src/Lean/Parser/Syntax.lean
+++ b/src/Lean/Parser/Syntax.lean
@@ -23,7 +23,7 @@ def «precedence» := parser! ":" >> precedenceLit
 def optPrecedence := optional (try «precedence»)
 
 namespace Syntax
-@[builtinSyntaxParser] def paren     := parser! "(" >> many1 syntaxParser >> ")"
+@[builtinSyntaxParser] def paren     := parser! symbol "(" appPrec >> many1 syntaxParser >> ")"
 @[builtinSyntaxParser] def cat       := parser! ident >> optPrecedence
 @[builtinSyntaxParser] def atom      := parser! strLit >> optPrecedence
 @[builtinSyntaxParser] def num       := parser! nonReservedSymbol "num"
@@ -38,7 +38,7 @@ namespace Syntax
 @[builtinSyntaxParser] def optional  := tparser! symbolAux "?" none
 @[builtinSyntaxParser] def many      := tparser! symbolAux "*" none
 @[builtinSyntaxParser] def many1     := tparser! symbolAux "+" none
-@[builtinSyntaxParser] def orelse    := tparser! " <|> " >> syntaxParser 1
+@[builtinSyntaxParser] def orelse    := tparser! symbol " <|> " 2 >> syntaxParser 1
 
 end Syntax
 
@@ -59,7 +59,7 @@ def mixfixSymbol := quotedSymbolPrec <|> unquotedSymbol
 def strLitPrec := parser! strLit >> optPrecedence
 def identPrec  := parser! ident >> optPrecedence
 
-def optKind : Parser := optional ("[" >> ident >> "]")
+def optKind : Parser := optional (symbol "[" appPrec >> ident >> "]")
 -- TODO: remove " := " after old frontend is gone
 @[builtinCommandParser] def «notation»    := parser! "notation" >> many (strLitPrec <|> quotedSymbolPrec <|> identPrec) >> (" := " <|> darrow) >> termParser
 @[builtinCommandParser] def «macro_rules» := parser! "macro_rules" >> optKind >> Term.matchAlts
@@ -69,9 +69,9 @@ def macroArgType   := nonReservedSymbol "ident" <|> nonReservedSymbol "num" <|>
 def macroArgSimple := parser! ident >> checkNoWsBefore "no space before ':'" >> ":" >> macroArgType
 def macroArg  := try strLitPrec <|> try macroArgSimple
 def macroHead := macroArg <|> try identPrec
-def macroTailTactic   : Parser := try (" : " >> identEq "tactic") >> darrow >>  "`(" >> sepBy1 tacticParser "; " true true >> ")"
-def macroTailCommand  : Parser := try (" : " >> identEq "command") >> darrow >> "`(" >> many1 commandParser true >> ")"
-def macroTailDefault  : Parser := try (" : " >> ident) >> darrow >> (("`(" >> categoryParserOfStack 2 >> ")") <|> termParser)
+def macroTailTactic   : Parser := try (" : " >> identEq "tactic") >> darrow >> symbol "`(" appPrec >> sepBy1 tacticParser "; " true true >> ")"
+def macroTailCommand  : Parser := try (" : " >> identEq "command") >> darrow >> symbol "`(" appPrec >> many1 commandParser true >> ")"
+def macroTailDefault  : Parser := try (" : " >> ident) >> darrow >> ((symbol "`(" appPrec >> categoryParserOfStack 2 >> ")") <|> termParser)
 def macroTail := macroTailTactic <|> macroTailCommand <|> macroTailDefault
 @[builtinCommandParser] def «macro»       := parser! "macro " >> macroHead >> many macroArg >> macroTail
 
diff --git a/src/Lean/Parser/Tactic.lean b/src/Lean/Parser/Tactic.lean
index d027c72800..d129c79044 100644
--- a/src/Lean/Parser/Tactic.lean
+++ b/src/Lean/Parser/Tactic.lean
@@ -37,7 +37,7 @@ def ident' : Parser := ident <|> underscore
 @[builtinTacticParser] def «skip»       := parser! nonReservedSymbol "skip"
 @[builtinTacticParser] def «traceState» := parser! nonReservedSymbol "traceState"
 @[builtinTacticParser] def «failIfSuccess» := parser! nonReservedSymbol "failIfSuccess " >> tacticParser
-@[builtinTacticParser] def «generalize» := parser! nonReservedSymbol "generalize" >> optional (try (ident >> " : ")) >> termParser 50 >> " = " >> ident
+@[builtinTacticParser] def «generalize» := parser! nonReservedSymbol "generalize" >> optional (try (ident >> " : ")) >> termParser 50 >> symbol " = " 50 >> ident
 def majorPremise := parser! optional (try (ident >> " : ")) >> termParser
 def inductionAlt  : Parser := nodeWithAntiquot "inductionAlt" `Lean.Parser.Tactic.inductionAlt $ ident' >> many ident' >> darrow >> (Term.hole <|> Term.namedHole <|> tacticParser)
 def inductionAlts : Parser := withPosition $ fun pos => "|" >> sepBy1 inductionAlt (checkColGe pos.column "alternatives must be indented" >> "|")
@@ -48,10 +48,10 @@ def generalizingVars := optional (" generalizing " >> many1 ident)
 @[builtinTacticParser] def «cases»      := parser! nonReservedSymbol "cases " >> majorPremise >> withAlts
 def withIds : Parser := optional (" with " >> many1 ident')
 @[builtinTacticParser] def «injection»  := parser! nonReservedSymbol "injection " >> termParser >> withIds
-@[builtinTacticParser] def paren        := parser! "(" >> nonEmptySeq >> ")"
-@[builtinTacticParser] def nestedTacticBlock := parser! "begin " >> seq >> "end"
-@[builtinTacticParser] def nestedTacticBlockCurly := parser! "{" >> seq >> "}"
-@[builtinTacticParser] def orelse := tparser! " <|> " >> tacticParser 1
+@[builtinTacticParser] def paren        := parser! symbol "(" appPrec  >> nonEmptySeq >> ")"
+@[builtinTacticParser] def nestedTacticBlock := parser! symbol "begin " appPrec >> seq >> "end"
+@[builtinTacticParser] def nestedTacticBlockCurly := parser! symbol "{" appPrec >> seq >> "}"
+@[builtinTacticParser] def orelse := tparser! symbol " <|> " 2 >> tacticParser 1
 
 end Tactic
 end Parser
diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean
index a7175a1853..bdc492d43e 100644
--- a/src/Lean/Parser/Term.lean
+++ b/src/Lean/Parser/Term.lean
@@ -47,7 +47,7 @@ def leadPrec := appPrec - 1
 -- NOTE: `checkNoWsBefore` should be used *before* `parser!` so that it is also applied to the generated
 -- antiquotation.
 def explicitUniv := checkNoWsBefore "no space before '.{'" >> parser! ".{" >> sepBy1 levelParser ", " >> "}"
-def namedPattern := checkNoWsBefore "no space before '@'" >> parser! "@" >> termParser appPrec
+def namedPattern := checkNoWsBefore "no space before '@'" >> parser! symbol "@" appPrec >> termParser appPrec
 @[builtinTermParser] def id := parser! ident >> optional (explicitUniv <|> namedPattern)
 @[builtinTermParser] def num : Parser := parser! numLit
 @[builtinTermParser] def str : Parser := parser! strLit
@@ -72,7 +72,7 @@ def haveAssign := parser! " := " >> termParser
 @[builtinTermParser] def «have» := parser! symbol "have " leadPrec >> optIdent >> termParser >> (haveAssign <|> fromTerm) >> "; " >> termParser
 @[builtinTermParser] def «suffices» := parser! symbol "suffices " leadPrec >> optIdent >> termParser >> fromTerm >> "; " >> termParser
 @[builtinTermParser] def «show»     := parser! symbol "show " leadPrec >> termParser >> fromTerm
-def structInstArrayRef := parser! "[" >> termParser >>"]"
+def structInstArrayRef := parser! symbol "[" appPrec >> termParser >>"]"
 def structInstLVal   := (ident <|> fieldIdx <|> structInstArrayRef) >> many (group ("." >> (ident <|> fieldIdx)) <|> structInstArrayRef)
 def structInstField  := parser! structInstLVal >> " := " >> termParser
 @[builtinTermParser] def structInst := parser! symbol "{" appPrec >> optional (try (termParser >> "with")) >> sepBy structInstField ", " true >> optional ".." >> optional (" : " >> termParser) >> "}"
@@ -85,11 +85,11 @@ def optType : Parser := optional typeSpec
 @[builtinTermParser] def inaccessible := parser! symbol ".(" appPrec >> termParser >> ")"
 def binderIdent : Parser  := ident <|> hole
 def binderType (requireType := false) : Parser := if requireType then group (" : " >> termParser) else optional (" : " >> termParser)
-def binderTactic  := parser! try (" := " >> " by ") >> Tactic.nonEmptySeq
+def binderTactic  := parser! try (" := " >> symbol " by " leadPrec) >> Tactic.nonEmptySeq
 def binderDefault := parser! " := " >> termParser
-def explicitBinder (requireType := false) := parser! "(" >> many1 binderIdent >> binderType requireType >> optional (binderTactic <|> binderDefault) >> ")"
-def implicitBinder (requireType := false) := parser! "{" >> many1 binderIdent >> binderType requireType >> "}"
-def instBinder := parser! "[" >> optIdent >> termParser >> "]"
+def explicitBinder (requireType := false) := parser! symbol "(" appPrec >> many1 binderIdent >> binderType requireType >> optional (binderTactic <|> binderDefault) >> ")"
+def implicitBinder (requireType := false) := parser! symbol "{" appPrec >> many1 binderIdent >> binderType requireType >> "}"
+def instBinder := parser! symbol "[" appPrec >> optIdent >> termParser >> "]"
 def bracketedBinder (requireType := false) := explicitBinder requireType <|> implicitBinder requireType <|> instBinder
 @[builtinTermParser] def depArrow := parser! bracketedBinder true >> checkRBPGreater 25 "expected parentheses around dependent arrow" >> unicodeSymbol " → " " -> " >> termParser
 def simpleBinder := parser! many1 binderIdent
@@ -126,13 +126,13 @@ def letDecl              := letIdDecl <|> letPatDecl <|> letEqnsDecl
 @[builtinTermParser] def «let!» := parser! symbol "let! " leadPrec >> letDecl >> "; " >> termParser
 
 def leftArrow : Parser := unicodeSymbol " ← " " <- "
-def doLet  := parser! "let " >> letDecl
+def doLet  := parser! symbol "let " leadPrec >> letDecl
 def doId   := parser! try (ident >> optType >> leftArrow) >> termParser
 def doPat  := parser! try (termParser >> leftArrow) >> termParser >> optional (" | " >> termParser)
 def doExpr := parser! termParser
 def doElem := doLet <|> doId <|> doPat <|> doExpr
 def doSeq  := sepBy1 doElem "; "
-def bracketedDoSeq := parser! "{" >> doSeq >> "}"
+def bracketedDoSeq := parser! symbol "{" appPrec >> doSeq >> "}"
 @[builtinTermParser] def liftMethod := parser! leftArrow >> termParser
 @[builtinTermParser] def «do»  := parser! symbol "do " leadPrec >> (bracketedDoSeq <|> doSeq)
 
@@ -145,7 +145,7 @@ def bracketedDoSeq := parser! "{" >> doSeq >> "}"
 -- symbol precedence should be higher, but must match the one of `sub` below
 @[builtinTermParser] def uminus := parser! symbol "-" 65 >> termParser 100
 
-def namedArgument  := parser! try ("(" >> ident >> " := ") >> termParser >> ")"
+def namedArgument  := parser! try (symbol "(" appPrec >> ident >> " := ") >> termParser >> ")"
 @[builtinTermParser] def app      := tparser! many1 (namedArgument <|> termParser appPrec)
 
 def checkIsSort := checkStackTop (fun stx => stx.isOfKind `Lean.Parser.Term.type || stx.isOfKind `Lean.Parser.Term.sort)
@@ -157,7 +157,7 @@ def checkIsSort := checkStackTop (fun stx => stx.isOfKind `Lean.Parser.Term.type
 @[builtinTermParser] def dollar     := tparser! try (dollarSymbol >> checkWsBefore "space expected") >> termParser 0
 @[builtinTermParser] def dollarProj := tparser! symbol "$." 1 >> (fieldIdx <|> ident)
 
-@[builtinTermParser] def «where»    := tparser! symbol " where " 1 >> sepBy1 letDecl (group ("; " >> " where "))
+@[builtinTermParser] def «where»    := tparser! symbol " where " 1 >> sepBy1 letDecl (group ("; " >> symbol " where " 1))
 
 @[builtinTermParser] def fcomp  := tparser! infixR " ∘ " 90
 
@@ -182,7 +182,7 @@ def checkIsSort := checkStackTop (fun stx => stx.isOfKind `Lean.Parser.Term.type
 @[builtinTermParser] def heq   := tparser! unicodeInfixL " ≅ " " ~= " 50
 @[builtinTermParser] def equiv := tparser! infixL " ≈ " 50
 
-@[builtinTermParser] def subst := tparser! symbol " ▸ " 75 >> sepBy1 (termParser 75) " ▸ "
+@[builtinTermParser] def subst := tparser! symbol " ▸ " 75 >> sepBy1 (termParser 75) (symbol " ▸ " 75)
 
 @[builtinTermParser] def and   := tparser! unicodeInfixR " ∧ " " /\\ " 35
 @[builtinTermParser] def or    := tparser! unicodeInfixR " ∨ " " \\/ " 30