diff --git a/src/Lean/Elab/Binders.lean b/src/Lean/Elab/Binders.lean
index 098fa73340..1b64c3774d 100644
--- a/src/Lean/Elab/Binders.lean
+++ b/src/Lean/Elab/Binders.lean
@@ -268,7 +268,7 @@ private partial def expandFunBindersAux (binders : Array Syntax) : Syntax → Na
 /--
   Auxiliary function for expanding `fun` notation binders. Recall that `fun` parser is defined as
   ```
-  def funBinder : Parser := implicitBinder <|> instBinder <|> termParser appPrec
+  def funBinder : Parser := implicitBinder <|> instBinder <|> termParser maxPrec
   parser! unicodeSymbol "λ" "fun" >> many1 funBinder >> "=>" >> termParser
   ```
   to allow notation such as `fun (a, b) => a + b`, where `(a, b)` should be treated as a pattern.
diff --git a/src/Lean/Elab/BuiltinNotation.lean b/src/Lean/Elab/BuiltinNotation.lean
index 5e458d8857..ad2ee31ddb 100644
--- a/src/Lean/Elab/BuiltinNotation.lean
+++ b/src/Lean/Elab/BuiltinNotation.lean
@@ -99,7 +99,7 @@ match extractMacroScopes declName with
 
 @[builtinTermElab «parser!»] def elabParserMacro : TermElab :=
 adaptExpander $ fun stx => match_syntax stx with
-| `(parser! $e)         => elabParserMacroAux stx (quote Parser.appPrec) e
+| `(parser! $e)         => elabParserMacroAux stx (quote Parser.maxPrec) e
 | `(parser! : $prec $e) => elabParserMacroAux stx prec e
 | _                     => throwUnsupportedSyntax
 
@@ -111,7 +111,7 @@ match declName? with
 
 @[builtinTermElab «tparser!»] def elabTParserMacro : TermElab :=
 adaptExpander $ fun stx => match_syntax stx with
-| `(tparser! $e)         => elabTParserMacroAux stx (quote Parser.appPrec) e
+| `(tparser! $e)         => elabTParserMacroAux stx (quote Parser.maxPrec) e
 | `(tparser! : $prec $e) => elabTParserMacroAux stx prec e
 | _                      => throwUnsupportedSyntax
 
diff --git a/src/Lean/Elab/Quotation.lean b/src/Lean/Elab/Quotation.lean
index d3e6077154..befac9a0ea 100644
--- a/src/Lean/Elab/Quotation.lean
+++ b/src/Lean/Elab/Quotation.lean
@@ -397,7 +397,7 @@ def oldParseExpr (env : Environment) (input : String) (pos : String.Pos) : Excep
 let c := Parser.mkParserContext env (Parser.mkInputContext input "<foo>");
 let s := Parser.mkParserState c.input;
 let s := s.setPos pos;
-let s := (Parser.termParser Parser.appPrec : Parser.Parser).fn { c with prec := Parser.appPrec } s;
+let s := (Parser.termParser Parser.maxPrec : Parser.Parser).fn { c with prec := Parser.maxPrec } s;
 let stx := s.stxStack.back;
 match s.errorMsg with
 | some errorMsg =>
diff --git a/src/Lean/Elab/StructInst.lean b/src/Lean/Elab/StructInst.lean
index 68424e2c07..cfc5d4536b 100644
--- a/src/Lean/Elab/StructInst.lean
+++ b/src/Lean/Elab/StructInst.lean
@@ -14,7 +14,7 @@ namespace Elab
 namespace Term
 namespace StructInst
 
-/- parser! symbol "{" appPrec >> optional (try (termParser >> "with")) >> sepBy structInstField ", " true >> optional ".." >> optional (" : " >> termParser) >> "}" -/
+/- parser! "{" >> optional (try (termParser >> "with")) >> sepBy structInstField ", " true >> optional ".." >> optional (" : " >> termParser) >> "}" -/
 
 /-
 If `stx` is of the form `{ s with ... }` and `s` is not a local variable, expand into `let src := s; { src with ... }`.
diff --git a/src/Lean/Elab/Syntax.lean b/src/Lean/Elab/Syntax.lean
index 72b01e7ce4..bbc242b9bb 100644
--- a/src/Lean/Elab/Syntax.lean
+++ b/src/Lean/Elab/Syntax.lean
@@ -15,13 +15,13 @@ namespace Term
 /-
 Expand `optional «precedence»` where
  «precedence» := parser! " : " >> precedenceLit
- precedenceLit : Parser := numLit <|> maxPrec
- maxPrec := parser! nonReservedSymbol "max" -/
+ precedenceLit : Parser := numLit <|> maxSymbol
+ maxSymbol := parser! nonReservedSymbol "max" -/
 def expandOptPrecedence (stx : Syntax) : Option Nat :=
 if stx.isNone then none
 else match ((stx.getArg 0).getArg 1).isNatLit? with
   | some v => some v
-  | _      => some Parser.appPrec
+  | _      => some Parser.maxPrec
 
 private def mkParserSeq (ds : Array Syntax) : TermElabM Syntax :=
 if ds.size == 0 then
@@ -192,7 +192,7 @@ fun stx => do
   env ← getEnv;
   let cat := (stx.getIdAt 5).eraseMacroScopes;
   unless (Parser.isParserCategory env cat) $ throwError (stx.getArg 5) ("unknown category '" ++ cat ++ "'");
-  let prec := (Term.expandOptPrecedence (stx.getArg 1)).getD Parser.appPrec;
+  let prec := (Term.expandOptPrecedence (stx.getArg 1)).getD Parser.maxPrec;
   kind ← elabKind (stx.getArg 2) cat;
   let catParserId := mkIdentFrom stx (cat.appendAfter "Parser");
   (val, trailingParser) ← runTermElabM none $ fun _ => Term.toParserDescr (stx.getArg 3) cat;
diff --git a/src/Lean/Parser/Level.lean b/src/Lean/Parser/Level.lean
index cf2601e40e..a442931758 100644
--- a/src/Lean/Parser/Level.lean
+++ b/src/Lean/Parser/Level.lean
@@ -18,8 +18,8 @@ categoryParser `level rbp
 namespace Level
 
 @[builtinLevelParser] def paren  := parser! "(" >> levelParser >> ")"
-@[builtinLevelParser] def max    := parser! nonReservedSymbol "max " true  >> many1 (levelParser appPrec)
-@[builtinLevelParser] def imax   := parser! nonReservedSymbol "imax " true >> many1 (levelParser appPrec)
+@[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    := parser! numLit
 @[builtinLevelParser] def ident  := parser! ident
diff --git a/src/Lean/Parser/Parser.lean b/src/Lean/Parser/Parser.lean
index 258f7613e0..c6100cac08 100644
--- a/src/Lean/Parser/Parser.lean
+++ b/src/Lean/Parser/Parser.lean
@@ -86,14 +86,14 @@ def getNext (input : String) (pos : Nat) : Char :=
 input.get (input.next pos)
 
 /- Function application precedence.
-   In the standard lean language, only two tokens have precedence higher that `appPrec`.
-   - The token `.` has precedence `appPrec+1`. Thus, field accesses like `g (h x).f` are parsed as `g ((h x).f)`,
+   In the standard lean language, only two tokens have precedence higher that `maxPrec`.
+   - The token `.` has precedence `maxPrec+1`. Thus, field accesses like `g (h x).f` are parsed as `g ((h x).f)`,
      not `(g (h x)).f`
-   - The token `[` when not preceded with whitespace has precedence `appPrec+1`. If there is whitespace before
-     `[`, then its precedence is `appPrec`. Thus, `f a[i]` is parsed as `f (a[i])` where `a[i]` is an "find-like operation"
+   - The token `[` when not preceded with whitespace has precedence `maxPrec+1`. If there is whitespace before
+     `[`, then its precedence is `maxPrec`. Thus, `f a[i]` is parsed as `f (a[i])` where `a[i]` is an "find-like operation"
       (e.g., array access, map access, etc.). `f a [i]` is parsed as `(f a) [i]` where `[i]` is a singleton collection
       (e.g., a list). -/
-def appPrec : Nat := 1024
+def maxPrec : Nat := 1024
 
 abbrev Token := String
 
@@ -1568,9 +1568,9 @@ partial def trailingLoop (tables : PrattParsingTables) (c : ParserContext) : Par
   As an extension of the original algorithm, we also check the current token's precedence before calling the leading
   parser(s). We do this so we can define an n-ary application parser:
   ```
-  @[builtinTermParser] def app := tparser! many1 (namedArgument <|> termParser appPrec)
+  @[builtinTermParser] def app := tparser! many1 (namedArgument <|> termParser maxPrec)
   ```
-  If the nested `termParser appPrec` did not check the precedence of the first token, we would accept bogus input such as
+  If the nested `termParser maxPrec` did not check the precedence of the first token, we would accept bogus input such as
   `f x fun y => y` because we would never check the precedence of `fun`. Note that, in contrast to trailing tokens, a
   leading token is accepted if its precedence is *at least* `prec`. This is necessary so that `f x y` is not parsed as
   `f (x y)`: the nested `termParser` call must accept the leading token `x` but not the trailing token `y`. But both have
diff --git a/src/Lean/Parser/Syntax.lean b/src/Lean/Parser/Syntax.lean
index 1b6a48ffb1..5e704e5f14 100644
--- a/src/Lean/Parser/Syntax.lean
+++ b/src/Lean/Parser/Syntax.lean
@@ -18,8 +18,8 @@ registerBuiltinParserAttribute `builtinSyntaxParser `syntax leadingIdentAsSymbol
 categoryParser `syntax rbp
 
 -- TODO: `max` is a bad precedence name. Find a new one.
-def maxPrec := parser! nonReservedSymbol "max" true
-def precedenceLit : Parser := numLit <|> maxPrec
+def maxSymbol := parser! nonReservedSymbol "max" true
+def precedenceLit : Parser := numLit <|> maxSymbol
 def «precedence» := parser! ":" >> precedenceLit
 def optPrecedence := optional (try «precedence»)
 
@@ -31,10 +31,10 @@ namespace Syntax
 @[builtinSyntaxParser] def str       := parser! nonReservedSymbol "str"
 @[builtinSyntaxParser] def char      := parser! nonReservedSymbol "char"
 @[builtinSyntaxParser] def ident     := parser! nonReservedSymbol "ident"
-@[builtinSyntaxParser] def try       := parser! nonReservedSymbol "try " >> syntaxParser appPrec
-@[builtinSyntaxParser] def lookahead := parser! nonReservedSymbol "lookahead " >> syntaxParser appPrec
-@[builtinSyntaxParser] def sepBy     := parser! nonReservedSymbol "sepBy " >> syntaxParser appPrec >> syntaxParser appPrec
-@[builtinSyntaxParser] def sepBy1    := parser! nonReservedSymbol "sepBy1 " >> syntaxParser appPrec >> syntaxParser appPrec
+@[builtinSyntaxParser] def try       := parser! nonReservedSymbol "try " >> syntaxParser maxPrec
+@[builtinSyntaxParser] def lookahead := parser! nonReservedSymbol "lookahead " >> syntaxParser maxPrec
+@[builtinSyntaxParser] def sepBy     := parser! nonReservedSymbol "sepBy " >> syntaxParser maxPrec >> syntaxParser maxPrec
+@[builtinSyntaxParser] def sepBy1    := parser! nonReservedSymbol "sepBy1 " >> syntaxParser maxPrec >> syntaxParser maxPrec
 
 @[builtinSyntaxParser] def optional  := tparser! "?"
 @[builtinSyntaxParser] def many      := tparser! "*"
diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean
index ea886a885e..e166e2eeee 100644
--- a/src/Lean/Parser/Term.lean
+++ b/src/Lean/Parser/Term.lean
@@ -41,19 +41,19 @@ checkPrec prec >> unicodeSymbol sym asciiSym >> termParser (prec+1)
 def infixL (sym : String) (prec : Nat) : TrailingParser :=
 checkPrec prec >> symbol sym >> termParser (prec+1)
 
-def leadPrec := appPrec - 1
+def leadPrec := maxPrec - 1
 
 /- Built-in parsers -/
 -- 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! "@" >> termParser maxPrec
 @[builtinTermParser] def id := parser! ident >> optional (explicitUniv <|> namedPattern)
 @[builtinTermParser] def num : Parser := parser! numLit
 @[builtinTermParser] def str : Parser := parser! strLit
 @[builtinTermParser] def char : Parser := parser! charLit
-@[builtinTermParser] def type := parser! "Type" >> optional (checkPrec (appPrec-1) >> levelParser appPrec)
-@[builtinTermParser] def sort := parser! "Sort" >> optional (checkPrec (appPrec-1) >> levelParser appPrec)
+@[builtinTermParser] def type := parser! "Type" >> optional (checkPrec (maxPrec-1) >> levelParser maxPrec)
+@[builtinTermParser] def sort := parser! "Sort" >> optional (checkPrec (maxPrec-1) >> levelParser maxPrec)
 @[builtinTermParser] def prop := parser! "Prop"
 @[builtinTermParser] def hole := parser! "_"
 @[builtinTermParser] def namedHole := parser! "?" >> ident
@@ -81,7 +81,7 @@ def optType : Parser := optional typeSpec
 @[builtinTermParser] def subtype := parser! "{" >> ident >> optType >> " // " >> termParser >> "}"
 @[builtinTermParser] def listLit := parser! "[" >> sepBy termParser "," true >> "]"
 @[builtinTermParser] def arrayLit := parser! "#[" >> sepBy termParser "," true >> "]"
-@[builtinTermParser] def explicit := parser! "@" >> termParser appPrec
+@[builtinTermParser] def explicit := parser! "@" >> termParser maxPrec
 @[builtinTermParser] def inaccessible := parser! ".(" >> termParser >> ")"
 def binderIdent : Parser  := ident <|> hole
 def binderType (requireType := false) : Parser := if requireType then group (" : " >> termParser) else optional (" : " >> termParser)
@@ -95,7 +95,7 @@ def bracketedBinder (requireType := false) := explicitBinder requireType <|> imp
 def simpleBinder := parser! many1 binderIdent
 @[builtinTermParser] def «forall» := parser!:leadPrec unicodeSymbol "∀" "forall" >> many1 (simpleBinder <|> bracketedBinder) >> ", " >> termParser
 
-def funBinder : Parser := implicitBinder <|> instBinder <|> termParser appPrec
+def funBinder : Parser := implicitBinder <|> instBinder <|> termParser maxPrec
 @[builtinTermParser] def «fun» := parser!:leadPrec unicodeSymbol "λ" "fun" >> many1 funBinder >> darrow >> termParser
 
 def matchAlt : Parser :=
@@ -109,10 +109,10 @@ withPosition $ fun pos =>
 
 @[builtinTermParser] def «match» := parser!:leadPrec "match " >> sepBy1 termParser ", " >> optType >> " with " >> matchAlts
 @[builtinTermParser] def «nomatch»  := parser!:leadPrec "nomatch " >> termParser
-def optExprPrecedence := optional (try ":" >> termParser appPrec)
+def optExprPrecedence := optional (try ":" >> termParser maxPrec)
 @[builtinTermParser] def «parser!»  := parser!:leadPrec "parser! " >> optExprPrecedence >> termParser
 @[builtinTermParser] def «tparser!» := parser!:leadPrec "tparser! " >> optExprPrecedence >> termParser
-@[builtinTermParser] def borrowed   := parser! "@&" >> termParser (appPrec - 1)
+@[builtinTermParser] def borrowed   := parser! "@&" >> termParser (maxPrec - 1)
 @[builtinTermParser] def quotedName := parser! nameLit
 -- NOTE: syntax quotations are defined in Init.Lean.Parser.Command
 @[builtinTermParser] def «match_syntax» := parser!:leadPrec "match_syntax" >> termParser >> " with " >> matchAlts
@@ -137,9 +137,9 @@ def bracketedDoSeq := parser! "{" >> doSeq >> "}"
 @[builtinTermParser] def liftMethod := parser!:0 leftArrow >> termParser
 @[builtinTermParser] def «do»  := parser!:leadPrec "do " >> (bracketedDoSeq <|> doSeq)
 
-@[builtinTermParser] def nativeRefl   := parser! "nativeRefl! " >> termParser appPrec
-@[builtinTermParser] def nativeDecide := parser! "nativeDecide! " >> termParser appPrec
-@[builtinTermParser] def decide       := parser! "decide! " >> termParser appPrec
+@[builtinTermParser] def nativeRefl   := parser! "nativeRefl! " >> termParser maxPrec
+@[builtinTermParser] def nativeDecide := parser! "nativeDecide! " >> termParser maxPrec
+@[builtinTermParser] def decide       := parser! "decide! " >> termParser maxPrec
 
 @[builtinTermParser] def not    := parser! "¬" >> termParser 40
 @[builtinTermParser] def bnot   := parser! "!" >> termParser 40
@@ -147,7 +147,7 @@ def bracketedDoSeq := parser! "{" >> doSeq >> "}"
 @[builtinTermParser] def uminus := parser!:65 "-" >> termParser 100
 
 def namedArgument  := parser! try ("(" >> ident >> " := ") >> termParser >> ")"
-@[builtinTermParser] def app      := tparser!:(appPrec-1) many1 (namedArgument <|> termParser appPrec)
+@[builtinTermParser] def app      := tparser!:(maxPrec-1) many1 (namedArgument <|> termParser maxPrec)
 
 @[builtinTermParser] def proj     := tparser! symbolNoWs "." >> (fieldIdx <|> ident)
 @[builtinTermParser] def arrow    := tparser! unicodeInfixR " → " " -> " 25
@@ -210,11 +210,11 @@ def namedArgument  := parser! try ("(" >> ident >> " := ") >> termParser >> ")"
 @[builtinTermParser] def byTactic    := parser!:leadPrec "by " >> Tactic.nonEmptySeq
 -- Use `unboxSingleton` trick similar to the one used at Command.lean for `Term.stxQuot`
 @[builtinTermParser] def tacticStxQuot    : Parser :=
-checkPrec appPrec >> (node `Lean.Parser.Term.stxQuot $ "`(tactic|" >> sepBy1 tacticParser "; " true true >> ")")
+checkPrec maxPrec >> (node `Lean.Parser.Term.stxQuot $ "`(tactic|" >> sepBy1 tacticParser "; " true true >> ")")
 @[builtinTermParser] def levelStxQuot     : Parser :=
-checkPrec appPrec >> (node `Lean.Parser.Term.stxQuot $ "`(level|" >> levelParser >> ")")
+checkPrec maxPrec >> (node `Lean.Parser.Term.stxQuot $ "`(level|" >> levelParser >> ")")
 @[builtinTermParser] def funBinderStxQuot : Parser :=
-checkPrec appPrec >> (node `Lean.Parser.Term.stxQuot $ "`(funBinder|"  >> funBinder >> ")")
+checkPrec maxPrec >> (node `Lean.Parser.Term.stxQuot $ "`(funBinder|"  >> funBinder >> ")")
 
 end Term
 end Parser
diff --git a/src/Lean/PrettyPrinter/Parenthesizer.lean b/src/Lean/PrettyPrinter/Parenthesizer.lean
index 2b33b176e3..8d2493299a 100644
--- a/src/Lean/PrettyPrinter/Parenthesizer.lean
+++ b/src/Lean/PrettyPrinter/Parenthesizer.lean
@@ -33,7 +33,7 @@ initial call to `checkRbpLe/Lt`, respectively. Thus we should parenthesize a syn
 Note that in case 2, it is also sufficient to parenthesize a *parent* node as long as the offending parser is still to
 the right of that node. For example, imagine the tree structure of `(f $ fun x => x) y` without parentheses. We need to
 insert *some* parentheses between `x` and `y` since the lambda body is parsed with precedence 0, while the identifier
-parser for `y` has precedence `appPrec`. But we need to parenthesize the `$` node anyway since the precedence of its
+parser for `y` has precedence `maxPrec`. But we need to parenthesize the `$` node anyway since the precedence of its
 RHS (0) again is smaller than that of `y`. So it's better to only parenthesize the outer node than ending up with
 `(f $ (fun x => x)) y`.
 
@@ -246,10 +246,10 @@ instance monadQuotation : MonadQuotation ParenthesizerM := {
 def visitAntiquot : ParenthesizerM Unit := do
 stx ← getCur;
 if Elab.Term.Quotation.isAntiquot stx then visitArgs $ do
-  -- antiquot syntax is, simplified, `syntax:appPrec "$" "$"* antiquotExpr ":" (nonReservedSymbol name) "*"?`
+  -- antiquot syntax is, simplified, `syntax:maxPrec "$" "$"* antiquotExpr ":" (nonReservedSymbol name) "*"?`
   goRight; goRight; -- now on `antiquotExpr`
   visit (mkConst `Lean.Parser.antiquotExpr);
-  addLbp appPrec
+  addLbp maxPrec
 else
   throw $ Exception.other $ "not an antiquotation"
 
@@ -282,7 +282,7 @@ when (rbp > minLbpP || match trailRbpP, trailLbp with some trailRbpP, some trail
     stx ← getCur; trace! `PrettyPrinter.parenthesize ("parenthesized: " ++ stx.formatStx none);
     goRight;
     -- after parenthesization, there is no more trailing parser
-    modify (fun st => { st with minLbp := appPrec, trailRbp := none })
+    modify (fun st => { st with minLbp := maxPrec, trailRbp := none })
 };
 modify $ fun stP => { stP with
   minLbp := match trailLbp with