diff --git a/library/init/lean/parser/parser.lean b/library/init/lean/parser/parser.lean index 23a8129481..09a5fcbbb3 100644 --- a/library/init/lean/parser/parser.lean +++ b/library/init/lean/parser/parser.lean @@ -726,7 +726,7 @@ match tk with def mkIdResult (startPos : Nat) (tk : Option TokenConfig) (val : Name) : BasicParserFn := fun c s => -let stopPos := s.pos; +let stopPos := s.pos; if isToken startPos stopPos tk then mkTokenAndFixPos startPos tk c s else @@ -769,7 +769,7 @@ partial def identFnAux (startPos : Nat) (tk : Option TokenConfig) : Name → Bas let s := s.next input s.pos; identFnAux r c s else - mkIdResult startPart tk r c s + mkIdResult startPos tk r c s else mkTokenAndFixPos startPos tk c s