diff --git a/src/Lean/Parser/Basic.lean b/src/Lean/Parser/Basic.lean
index 2ec988c507..3bd6ca879b 100644
--- a/src/Lean/Parser/Basic.lean
+++ b/src/Lean/Parser/Basic.lean
@@ -88,6 +88,7 @@ input.get (input.next pos)
    Note that nothing prevents users from using a higher precedence, but we strongly
    discourage them from doing it. -/
 def maxPrec : Nat := 1024
+def leadPrec := maxPrec - 1
 
 abbrev Token := String
 
@@ -351,6 +352,13 @@ instance hasAndthen : HasAndthen Parser :=
 { info := nodeInfo n p.info,
   fn   := nodeFn n p.fn }
 
+def errorFn (msg : String) : ParserFn :=
+fun _ s => s.mkUnexpectedError msg
+
+@[inline] def error (msg : String) : Parser :=
+{ info := epsilonInfo,
+  fn   := errorFn msg }
+
 /- Succeeds if `c.prec <= prec` -/
 def checkPrecFn (prec : Nat) : ParserFn :=
 fun c s =>
@@ -399,14 +407,14 @@ checkPrec prec >> trailingNodeAux n p
 @[inline] def group (p : Parser) : Parser :=
 node nullKind p
 
-def mergeOrElseErrors (s : ParserState) (error1 : Error) (iniPos : Nat) : ParserState :=
+def mergeOrElseErrors (s : ParserState) (error1 : Error) (iniPos : Nat) (mergeErrors : Bool) : ParserState :=
 match s with
 | ⟨stack, pos, cache, some error2⟩ =>
-  if pos == iniPos then ⟨stack, pos, cache, some (error1.merge error2)⟩
+  if pos == iniPos then ⟨stack, pos, cache, some (if mergeErrors then error1.merge error2 else error2)⟩
   else s
 | other => other
 
-@[inline] def orelseFn (p q : ParserFn) : ParserFn
+@[inline] def orelseFnCore (p q : ParserFn) (mergeErrors : Bool) : ParserFn
 | c, s =>
   let iniSz  := s.stackSize;
   let iniPos := s.pos;
@@ -414,11 +422,14 @@ match s with
   match s.errorMsg with
   | some errorMsg =>
     if s.pos == iniPos then
-      mergeOrElseErrors (q c (s.restore iniSz iniPos)) errorMsg iniPos
+      mergeOrElseErrors (q c (s.restore iniSz iniPos)) errorMsg iniPos mergeErrors
     else
       s
   | none => s
 
+@[inline] def orelseFn (p q : ParserFn) : ParserFn :=
+orelseFnCore p q true
+
 @[noinline] def orelseInfo (p q : ParserInfo) : ParserInfo :=
 { collectTokens := p.collectTokens ∘ q.collectTokens,
   collectKinds  := p.collectKinds ∘ q.collectKinds,
diff --git a/src/Lean/Parser/Module.lean b/src/Lean/Parser/Module.lean
index 71e39b7912..792460dc71 100644
--- a/src/Lean/Parser/Module.lean
+++ b/src/Lean/Parser/Module.lean
@@ -70,6 +70,12 @@ match s.errorMsg with
 | some _ => pos + 1
 | none   => s.pos
 
+def topLevelCommandParserFn : ParserFn :=
+orelseFnCore
+  commandParser.fn
+  (andthenFn (lookaheadFn termParser.fn) (errorFn "expected command, but found term; this error may be due to parsing precedence levels, consider parenthesizing the term"))
+  false /- do not merge errors -/
+
 partial def parseCommand (env : Environment) (inputCtx : InputContext) : ModuleParserState → MessageLog → Syntax × ModuleParserState × MessageLog
 | s@{ pos := pos, recovering := recovering }, messages =>
   if inputCtx.input.atEnd pos then
@@ -78,7 +84,7 @@ partial def parseCommand (env : Environment) (inputCtx : InputContext) : ModuleP
     let c  := mkParserContext env inputCtx;
     let s  := { cache := initCacheForInput c.input, pos := pos : ParserState };
     let s  := whitespace c s;
-    let s  := (commandParser : Parser).fn c s;
+    let s  := topLevelCommandParserFn c s;
     match s.errorMsg with
     | none =>
       let stx := s.stxStack.back;
diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean
index e15d2d541a..28266684df 100644
--- a/src/Lean/Parser/Term.lean
+++ b/src/Lean/Parser/Term.lean
@@ -41,8 +41,6 @@ checkPrec prec >> unicodeSymbol sym asciiSym >> termParser (prec+1)
 def infixL (sym : String) (prec : Nat) : TrailingParser :=
 checkPrec prec >> symbol sym >> termParser (prec+1)
 
-def leadPrec := maxPrec - 1
-
 /- Built-in parsers -/
 
 @[builtinTermParser] def byTactic := parser!:leadPrec "by " >> Tactic.indentedNonEmptySeq
@@ -52,8 +50,8 @@ def leadPrec := maxPrec - 1
 @[builtinTermParser] def num : Parser := checkPrec maxPrec >> numLit
 @[builtinTermParser] def str : Parser := checkPrec maxPrec >> strLit
 @[builtinTermParser] def char : Parser := checkPrec maxPrec >> 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 type := parser! "Type" >> optional (checkWsBefore "" >> checkPrec leadPrec >> levelParser maxPrec)
+@[builtinTermParser] def sort := parser! "Sort" >> optional (checkWsBefore "" >> checkPrec leadPrec >> levelParser maxPrec)
 @[builtinTermParser] def prop := parser! "Prop"
 @[builtinTermParser] def hole := parser! "_"
 @[builtinTermParser] def syntheticHole := parser! "?" >> (ident <|> hole)
@@ -135,7 +133,7 @@ def funBinder : Parser := funImplicitBinder <|> instBinder <|> termParser maxPre
 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 (maxPrec - 1)
+@[builtinTermParser] def borrowed   := parser! "@&" >> termParser leadPrec
 @[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
diff --git a/tests/lean/precissues.lean b/tests/lean/precissues.lean
index 4cc4bbc3e6..d91a5302e6 100644
--- a/tests/lean/precissues.lean
+++ b/tests/lean/precissues.lean
@@ -14,6 +14,8 @@ def f (x : Nat) (g : Nat → Nat) := g x
 
 #check id have True from ⟨⟩; this -- should fail
 
+#check id let x := 10; x
+
 #check 1
 
 #check id (have True from ⟨⟩; this)
diff --git a/tests/lean/precissues.lean.expected.out b/tests/lean/precissues.lean.expected.out
index 30eb0c26e7..6ffeab106d 100644
--- a/tests/lean/precissues.lean.expected.out
+++ b/tests/lean/precissues.lean.expected.out
@@ -4,7 +4,9 @@ f 1 fun (x : Nat) => x : Nat
 0 : Nat
 f 1 fun (x : Nat) => x : Nat
 id : ?m → ?m
-precissues.lean:15:10: error: expected command
+precissues.lean:15:10: error: expected command, but found term; this error may be due to parsing precedence levels, consider parenthesizing the term
+id : ?m → ?m
+precissues.lean:17:10: error: expected command, but found term; this error may be due to parsing precedence levels, consider parenthesizing the term
 1 : Nat
 id ((fun (this : True) => this) True.intro) : True
 0 = (fun (this : Nat) => this) 1 : Prop