diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean
index 1ae4d3f2e7..f0439b3c18 100644
--- a/src/Lean/Parser/Command.lean
+++ b/src/Lean/Parser/Command.lean
@@ -88,7 +88,7 @@ def openSimple       := parser! many1 ident
 @[builtinCommandParser] def «open»    := parser! "open " >> (openHiding <|> openRenaming <|> openOnly <|> openSimple)
 
 @[builtinCommandParser] def «mutual» := parser! "mutual " >> many1 (notFollowedBy «end» >> commandParser) >> "end"
-@[builtinCommandParser] def «initialize» := parser! "initialize " >> optional (ident >> Term.typeSpec >> Term.leftArrow) >> termParser
+@[builtinCommandParser] def «initialize» := parser! "initialize " >> optional (ident >> Term.typeSpec >> Term.leftArrow) >> Term.doSeq
 
 @[builtinCommandParser] def «in»  := tparser! " in " >> commandParser