diff --git a/src/Lean/Parser/Do.lean b/src/Lean/Parser/Do.lean
index f6fe09f6b2..78d951bf98 100644
--- a/src/Lean/Parser/Do.lean
+++ b/src/Lean/Parser/Do.lean
@@ -95,6 +95,7 @@ Note that parser priorities would not solve this problem since the `doIf` parser
 parser is succeeding.
 -/
 @[builtinDoElemParser] def doExpr   := parser! notFollowedByRedefinedTermToken >> termParser
+@[builtinDoElemParser] def doNested := parser! "do " >> doSeq
 
 @[builtinTermParser] def «do»  := parser!:maxPrec "do " >> doSeq