diff --git a/src/Lean/Parser/Do.lean b/src/Lean/Parser/Do.lean index 6a72c625d5..246d528f2d 100644 --- a/src/Lean/Parser/Do.lean +++ b/src/Lean/Parser/Do.lean @@ -70,7 +70,7 @@ def letIdDeclNoBinders := node ``letIdDecl <| @[builtin_doElem_parser] def doReassign := leading_parser notFollowedByRedefinedTermToken >> (letIdDeclNoBinders <|> letPatDecl) @[builtin_doElem_parser] def doReassignArrow := leading_parser - notFollowedByRedefinedTermToken >> withPosition (doIdDecl <|> doPatDecl) + notFollowedByRedefinedTermToken >> (doIdDecl <|> doPatDecl) @[builtin_doElem_parser] def doHave := leading_parser "have " >> Term.haveDecl /-