diff --git a/src/Lean/Parser/Basic.lean b/src/Lean/Parser/Basic.lean
index b39b5860bb..32012ec56d 100644
--- a/src/Lean/Parser/Basic.lean
+++ b/src/Lean/Parser/Basic.lean
@@ -125,6 +125,7 @@ structure ParserContext extends InputContext :=
 (env        : Environment)
 (tokens     : TokenTable)
 (insideQuot : Bool := false)
+(savedPos   : Position := { line := 1, column := 0 })
 
 structure Error :=
 (unexpected : String := "")
@@ -1373,29 +1374,30 @@ def anyOfFn : List Parser → ParserFn
 | [p],   c, s => p.fn c s
 | p::ps, c, s => orelseFn p.fn (anyOfFn ps) c s
 
-@[inline] def checkColGeFn (col : Nat) (errorMsg : String) : ParserFn :=
+
+@[inline] def checkColGeFn (errorMsg : String) : ParserFn :=
 fun c s =>
   let pos := c.fileMap.toPosition s.pos;
-  if pos.column ≥ col then s
+  if pos.column ≥ c.savedPos.column then s
   else s.mkError errorMsg
 
-@[inline] def checkColGe (col : Nat) (errorMsg : String) : Parser :=
-{ fn := checkColGeFn col errorMsg }
+@[inline] def checkColGe (errorMsg : String) : Parser :=
+{ fn := checkColGeFn errorMsg }
 
-@[inline] def checkLineLeFn (line : Nat) (errorMsg : String) : ParserFn :=
+@[inline] def checkColGtFn (errorMsg : String) : ParserFn :=
 fun c s =>
   let pos := c.fileMap.toPosition s.pos;
-  if pos.line ≤ line then s
+  if pos.column > c.savedPos.column then s
   else s.mkError errorMsg
 
-@[inline] def checkLineLe (line : Nat) (errorMsg : String) : Parser :=
-{ fn := checkLineLeFn line errorMsg }
+@[inline] def checkColGt (errorMsg : String) : Parser :=
+{ fn := checkColGtFn errorMsg }
 
-@[inline] def withPosition (p : Position → Parser) : Parser :=
-{ info := (p { line := 1, column := 0 }).info,
+@[inline] def withPosition (p : Parser) : Parser :=
+{ info := p.info,
   fn   := fun c s =>
    let pos := c.fileMap.toPosition s.pos;
-   (p pos).fn c s }
+   p.fn { c with savedPos := pos } s }
 
 def eoiFn : ParserFn :=
 fun c s =>
@@ -1407,7 +1409,7 @@ fun c s =>
 { fn := eoiFn }
 
 @[inline] def many1Indent (p : Parser) (errorMsg : String) : Parser :=
-withPosition $ fun pos => many1 (checkColGe pos.column errorMsg >> p)
+withPosition $ many1 (checkColGe errorMsg >> p)
 
 open Std (RBMap RBMap.empty)
 
diff --git a/src/Lean/Parser/Do.lean b/src/Lean/Parser/Do.lean
index 83eaa4b682..95e1c1cf2b 100644
--- a/src/Lean/Parser/Do.lean
+++ b/src/Lean/Parser/Do.lean
@@ -71,13 +71,13 @@ def leftArrow : Parser := unicodeSymbol " ← " " <- "
   `notFollowedByTermToken >> notFollowedBy (ident <|> numLit <|> strLit <|> charLit <|> nameLit)`
 -/
 def doSeqIndent :=
-withPosition fun pos₁ =>
+withPosition $
   sepBy1
     doElemParser
     -- The separator for the indented `do`-block
     ("; "
      -- check indentation
-     >> checkColGe pos₁.column "do-elements must be indented"
+     >> checkColGe "do-elements must be indented"
      >> notFollowedByCommandToken >> notFollowedBy eoi)
   >> optional (try ("; " >> notFollowedByTermToken >> notFollowedBy (ident <|> numLit <|> strLit <|> charLit <|> nameLit)))
 def doSeqBracketed := parser! "{" >> sepBy1 doElemParser "; " true >> "}"
@@ -117,15 +117,15 @@ else if c_2 then
        action_3
 ```
 -/
-@[builtinDoElemParser] def doIf := parser! withPosition fun pos =>
+@[builtinDoElemParser] def doIf := parser! withPosition $
   "if " >> termParser >> " then " >> doSeq
-  >> many (checkColGe pos.column "'else if' in 'do' must be indented" >> try (" else " >> " if ") >> termParser >> " then " >> doSeq)
-  >> optional (checkColGe pos.column "'else' in 'do' must be indented" >> " else " >> doSeq)
+  >> many (checkColGe "'else if' in 'do' must be indented" >> try (" else " >> " if ") >> termParser >> " then " >> doSeq)
+  >> optional (checkColGe "'else' in 'do' must be indented" >> " else " >> doSeq)
 @[builtinDoElemParser] def doFor   := parser! "for " >> termParser >> " in " >> termParser maxPrec >> doSeq
 
 /- `match`-expression where the right-hand-side of alternatives is a `doSeq` instead of a `term` -/
 def doMatchAlt : Parser  := sepBy1 termParser ", " >> darrow >> doSeq
-def doMatchAlts : Parser := parser! withPosition fun pos => (optional "| ") >> sepBy1 doMatchAlt (checkColGe pos.column "alternatives must be indented" >> "|")
+def doMatchAlts : Parser := parser! withPosition $ (optional "| ") >> sepBy1 doMatchAlt (checkColGe "alternatives must be indented" >> "|")
 @[builtinDoElemParser] def doMatch := parser!:leadPrec "match " >> sepBy1 matchDiscr ", " >> optType >> " with " >> doMatchAlts
 
 @[builtinDoElemParser] def «break» := parser! "break"
diff --git a/src/Lean/Parser/Tactic.lean b/src/Lean/Parser/Tactic.lean
index 3cf8e4c27b..ee08d9b94e 100644
--- a/src/Lean/Parser/Tactic.lean
+++ b/src/Lean/Parser/Tactic.lean
@@ -63,7 +63,7 @@ def rwRuleSeq := parser! "[" >> sepBy1 rwRule ", " true >> "]"
 def majorPremise := parser! optional (try (ident >> " : ")) >> termParser
 def altRHS := Term.hole <|> Term.syntheticHole <|> indentedNonEmptySeq
 def inductionAlt  : Parser := nodeWithAntiquot "inductionAlt" `Lean.Parser.Tactic.inductionAlt $ ident' >> many ident' >> darrow >> altRHS
-def inductionAlts : Parser := withPosition $ fun pos => "|" >> sepBy1 inductionAlt (checkColGe pos.column "alternatives must be indented" >> "|")
+def inductionAlts : Parser := withPosition $ "|" >> sepBy1 inductionAlt (checkColGe "alternatives must be indented" >> "|")
 def withAlts : Parser := optional (" with " >> inductionAlts)
 def usingRec : Parser := optional (" using " >> ident)
 def generalizingVars := optional (" generalizing " >> many1 ident)
@@ -71,7 +71,7 @@ def generalizingVars := optional (" generalizing " >> many1 ident)
 @[builtinTacticParser] def «cases»      := parser! nonReservedSymbol "cases " >> majorPremise >> withAlts
 
 def matchAlt  : Parser := parser! sepBy1 termParser ", " >> darrow >> altRHS
-def matchAlts : Parser := group $ withPosition $ fun pos => (optional "| ") >> sepBy1 matchAlt (checkColGe pos.column "alternatives must be indented" >> "|")
+def matchAlts : Parser := group $ withPosition $ (optional "| ") >> sepBy1 matchAlt (checkColGe "alternatives must be indented" >> "|")
 @[builtinTacticParser] def «match»      := parser! nonReservedSymbol "match " >> sepBy1 Term.matchDiscr ", " >> Term.optType >> " with " >> matchAlts
 @[builtinTacticParser] def «introMatch» := parser! nonReservedSymbol "intro " >> matchAlts
 
diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean
index 1825692c79..2ea5fb4de5 100644
--- a/src/Lean/Parser/Term.lean
+++ b/src/Lean/Parser/Term.lean
@@ -20,8 +20,8 @@ registerBuiltinDynamicParserAttribute `tacticParser `tactic
 categoryParser `tactic rbp
 
 def Tactic.indentedNonEmptySeq : Parser :=
-nodeWithAntiquot "tacticSeq" `Lean.Parser.Tactic.seq $ withPosition fun pos =>
-  sepBy1 tacticParser (try ("; " >>  checkColGe pos.column "tatic must be indented"))
+nodeWithAntiquot "tacticSeq" `Lean.Parser.Tactic.seq $ withPosition $
+  sepBy1 tacticParser (try ("; " >>  checkColGe "tatic must be indented"))
 
 def darrow : Parser := " => "
 
@@ -117,9 +117,9 @@ nodeWithAntiquot "matchAlt" `Lean.Parser.Term.matchAlt $
   sepBy1 termParser ", " >> darrow >> termParser
 
 def matchAlts (optionalFirstBar := true) : Parser :=
-parser! withPosition fun pos =>
+parser! withPosition $
   (if optionalFirstBar then optional "| " else "| ") >>
-  sepBy1 matchAlt (checkColGe pos.column "alternatives must be indented" >> "|")
+  sepBy1 matchAlt (checkColGe "alternatives must be indented" >> "|")
 
 def matchDiscr := parser! optional (try (ident >> checkNoWsBefore "no space before ':'" >> ":")) >> termParser
 
diff --git a/src/Lean/PrettyPrinter/Formatter.lean b/src/Lean/PrettyPrinter/Formatter.lean
index 76fd5ff521..079887373c 100644
--- a/src/Lean/PrettyPrinter/Formatter.lean
+++ b/src/Lean/PrettyPrinter/Formatter.lean
@@ -365,9 +365,8 @@ if stx.getKind == k then do
 else
   p
 
-@[combinatorFormatter Lean.Parser.withPosition] def withPosition.formatter (p : Position → Formatter) : Formatter := do
--- call closure with dummy position
-p ⟨0, 0⟩
+@[combinatorFormatter Lean.Parser.withPosition] def withPosition.formatter (p : Formatter) : Formatter := do
+p
 
 @[combinatorFormatter Lean.Parser.setExpected]
 def setExpected.formatter (expected : List String) (p : Formatter) : Formatter :=
@@ -386,7 +385,8 @@ pushLine
 @[combinatorFormatter checkNoWsBefore] def checkNoWsBefore.formatter : Formatter := pure ()
 @[combinatorFormatter checkTailWs] def checkTailWs.formatter : Formatter := pure ()
 @[combinatorFormatter checkColGe] def checkColGe.formatter : Formatter := pure ()
-@[combinatorFormatter checkLineLe] def checkLineLe.formatter : Formatter := pure ()
+@[combinatorFormatter checkColGt] def checkColGt.formatter : Formatter := pure ()
+
 @[combinatorFormatter eoi] def eoi.formatter : Formatter := pure ()
 @[combinatorFormatter notFollowedByCategoryToken] def notFollowedByCategoryToken.formatter : Formatter := pure ()
 @[combinatorFormatter checkNoImmediateColon] def checkNoImmediateColon.formatter : Formatter := pure ()
diff --git a/src/Lean/PrettyPrinter/Parenthesizer.lean b/src/Lean/PrettyPrinter/Parenthesizer.lean
index ea08ea08b4..e78d7632a8 100644
--- a/src/Lean/PrettyPrinter/Parenthesizer.lean
+++ b/src/Lean/PrettyPrinter/Parenthesizer.lean
@@ -430,9 +430,8 @@ if stx.getKind == k then
 else
   p
 
-@[combinatorParenthesizer Lean.Parser.withPosition] def withPosition.parenthesizer (p : Position → Parenthesizer) : Parenthesizer := do
--- call closure with dummy position
-p ⟨0, 0⟩
+@[combinatorParenthesizer Lean.Parser.withPosition] def withPosition.parenthesizer (p : Parenthesizer) : Parenthesizer := do
+p
 
 @[combinatorParenthesizer Lean.Parser.setExpected]
 def setExpected.parenthesizer (expected : List String) (p : Parenthesizer) : Parenthesizer :=
@@ -447,9 +446,9 @@ p
 @[combinatorParenthesizer Lean.Parser.checkNoWsBefore] def checkNoWsBefore.parenthesizer : Parenthesizer := pure ()
 @[combinatorParenthesizer Lean.Parser.checkTailWs] def checkTailWs.parenthesizer : Parenthesizer := pure ()
 @[combinatorParenthesizer Lean.Parser.checkColGe] def checkColGe.parenthesizer : Parenthesizer := pure ()
+@[combinatorParenthesizer Lean.Parser.checkColGt] def checkColGt.parenthesizer : Parenthesizer := pure ()
 @[combinatorParenthesizer Lean.Parser.eoi] def eoi.parenthesizer : Parenthesizer := pure ()
 @[combinatorParenthesizer Lean.Parser.notFollowedByCategoryToken] def notFollowedByCategoryToken.parenthesizer : Parenthesizer := pure ()
-@[combinatorParenthesizer Lean.Parser.checkLineLe] def checkLineLe.parenthesizer : Parenthesizer := pure ()
 @[combinatorParenthesizer Lean.Parser.checkNoImmediateColon] def checkNoImmediateColon.parenthesizer : Parenthesizer := pure ()
 @[combinatorParenthesizer Lean.Parser.checkInsideQuot] def checkInsideQuot.parenthesizer : Parenthesizer := pure ()
 @[combinatorParenthesizer Lean.Parser.checkOutsideQuot] def checkOutsideQuot.parenthesizer : Parenthesizer := pure ()