diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean
index bec2f52a88..8e041b9fe7 100644
--- a/src/Lean/Parser/Command.lean
+++ b/src/Lean/Parser/Command.lean
@@ -96,6 +96,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 «in»  := tparser! " in " >> commandParser