diff --git a/src/Lean/Parser/Basic.lean b/src/Lean/Parser/Basic.lean
index b86a272a81..208dde4de7 100644
--- a/src/Lean/Parser/Basic.lean
+++ b/src/Lean/Parser/Basic.lean
@@ -129,7 +129,7 @@ structure ParserContext extends InputContext :=
   (tokens             : TokenTable)
   (insideQuot         : Bool := false)
   (suppressInsideQuot : Bool := false)
-  (savedPos?          : Option Position := none)
+  (savedPos?          : Option String.Pos := none)
   (forbiddenTk?       : Option Token := none)
 
 structure Error :=
@@ -366,6 +366,21 @@ def errorFn (msg : String) : ParserFn := fun _ s =>
   fn   := errorFn msg
 }
 
+def errorAtSavedPosFn (msg : String) (delta : Bool) : ParserFn := fun c s =>
+  match c.savedPos? with
+  | none     => s
+  | some pos =>
+    let pos := if delta then c.input.next pos else pos
+    match s with
+    | ⟨stack, _, cache, _⟩ => ⟨stack, pos, cache, some { unexpected := msg }⟩
+
+/- Generate an error at the position saved with the `withPosition` combinator.
+   If `delta == true`, then it reports at saved position+1.
+   This useful to make sure a parser consumed at least one character.  -/
+@[inline] def errorAtSavedPos (msg : String) (delta : Bool) : Parser := {
+  fn := errorAtSavedPosFn msg delta
+}
+
 /- Succeeds if `c.prec <= prec` -/
 def checkPrecFn (prec : Nat) : ParserFn := fun c s =>
   if c.prec <= prec then s
@@ -1332,7 +1347,8 @@ def anyOfFn : List Parser → ParserFn
   match c.savedPos? with
   | none => s
   | some savedPos =>
-    let pos := c.fileMap.toPosition s.pos
+    let savedPos := c.fileMap.toPosition savedPos
+    let pos      := c.fileMap.toPosition s.pos
     if pos.column ≥ savedPos.column then s
     else s.mkError errorMsg
 
@@ -1343,7 +1359,8 @@ def anyOfFn : List Parser → ParserFn
   match c.savedPos? with
   | none => s
   | some savedPos =>
-    let pos := c.fileMap.toPosition s.pos
+    let savedPos := c.fileMap.toPosition savedPos
+    let pos      := c.fileMap.toPosition s.pos
     if pos.column > savedPos.column then s
     else s.mkError errorMsg
 
@@ -1354,7 +1371,8 @@ def anyOfFn : List Parser → ParserFn
   match c.savedPos? with
   | none => s
   | some savedPos =>
-    let pos := c.fileMap.toPosition s.pos
+    let savedPos := c.fileMap.toPosition savedPos
+    let pos      := c.fileMap.toPosition s.pos
     if pos.line == savedPos.line then s
     else s.mkError errorMsg
 
@@ -1364,8 +1382,7 @@ def anyOfFn : List Parser → ParserFn
 @[inline] def withPosition (p : Parser) : Parser := {
   info := p.info,
   fn   := fun c s =>
-    let pos := c.fileMap.toPosition s.pos
-    p.fn { c with savedPos? := pos } s
+    p.fn { c with savedPos? := s.pos } s
 }
 
 @[inline] def withoutPosition (p : Parser) : Parser := {
diff --git a/src/Lean/Parser/Tactic.lean b/src/Lean/Parser/Tactic.lean
index 925a47af0a..96727fc801 100644
--- a/src/Lean/Parser/Tactic.lean
+++ b/src/Lean/Parser/Tactic.lean
@@ -43,6 +43,7 @@ def ident' : Parser := ident <|> underscore
 @[builtinTacticParser] def «traceState» := parser! nonReservedSymbol "traceState"
 @[builtinTacticParser] def «failIfSuccess» := parser! nonReservedSymbol "failIfSuccess " >> tacticSeq
 @[builtinTacticParser] def «generalize» := parser! nonReservedSymbol "generalize " >> optional («try» (ident >> " : ")) >> termParser 51 >> " = " >> ident
+@[builtinTacticParser] def «unknown»    := parser! withPosition (ident >> errorAtSavedPos "unknown tactic" true)
 
 def locationWildcard := parser! "*"
 def locationTarget   := parser! unicodeSymbol "⊢" "|-"
diff --git a/src/Lean/PrettyPrinter/Formatter.lean b/src/Lean/PrettyPrinter/Formatter.lean
index 30bebb2bab..6e641d4246 100644
--- a/src/Lean/PrettyPrinter/Formatter.lean
+++ b/src/Lean/PrettyPrinter/Formatter.lean
@@ -192,6 +192,8 @@ def categoryParserOfStack.formatter (offset : Nat) : Formatter := do
 
 @[combinatorFormatter Lean.Parser.error]
 def error.formatter (msg : String) : Formatter := pure ()
+@[combinatorFormatter Lean.Parser.errorAtSavedPos]
+def errorAtSavedPos.formatter (msg : String) (delta : Bool) : Formatter := pure ()
 @[combinatorFormatter Lean.Parser.try]
 def try.formatter (p : Formatter) : Formatter := p
 @[combinatorFormatter Lean.Parser.lookahead]
diff --git a/src/Lean/PrettyPrinter/Parenthesizer.lean b/src/Lean/PrettyPrinter/Parenthesizer.lean
index 2d51f0fe85..b279216f0d 100644
--- a/src/Lean/PrettyPrinter/Parenthesizer.lean
+++ b/src/Lean/PrettyPrinter/Parenthesizer.lean
@@ -330,6 +330,10 @@ def level.parenthesizer : CategoryParenthesizer | prec => do
 def error.parenthesizer (msg : String) : Parenthesizer :=
   pure ()
 
+@[combinatorParenthesizer Lean.Parser.errorAtSavedPos]
+def errorAtSavedPos.parenthesizer (msg : String) (delta : Bool) : Parenthesizer :=
+  pure ()
+
 @[combinatorParenthesizer Lean.Parser.try]
 def try.parenthesizer (p : Parenthesizer) : Parenthesizer :=
   p
diff --git a/tests/lean/unknownTactic.lean b/tests/lean/unknownTactic.lean
new file mode 100644
index 0000000000..0fdd4d3be3
--- /dev/null
+++ b/tests/lean/unknownTactic.lean
@@ -0,0 +1,15 @@
+theorem ex1 (x : Nat) : x = x → x = x := by
+  intro
+  aexact (rfl)
+
+#print "---"
+
+theorem ex2 (x : Nat) : x = x → x = x :=
+  have x = x by foo
+  fun h => h
+
+#print "---"
+
+theorem ex3 (x : Nat) : x = x → x = x :=
+  have x = x by foo (aaa bbb)
+  fun h => h
diff --git a/tests/lean/unknownTactic.lean.expected.out b/tests/lean/unknownTactic.lean.expected.out
new file mode 100644
index 0000000000..da22471d63
--- /dev/null
+++ b/tests/lean/unknownTactic.lean.expected.out
@@ -0,0 +1,5 @@
+unknownTactic.lean:3:3: error: unknown tactic
+---
+unknownTactic.lean:8:17: error: unknown tactic
+---
+unknownTactic.lean:14:17: error: unknown tactic