diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean
index 6563d65c03..99d4a03ff5 100644
--- a/src/Lean/Parser/Command.lean
+++ b/src/Lean/Parser/Command.lean
@@ -113,11 +113,11 @@ def optionValue := nonReservedSymbol "true" <|> nonReservedSymbol "false" <|> st
 @[builtinCommandParser] def «set_option»   := leading_parser "set_option " >> ident >> ppSpace >> optionValue
 def eraseAttr := leading_parser "-" >> rawIdent
 @[builtinCommandParser] def «attribute»    := leading_parser "attribute " >> "[" >> sepBy1 (eraseAttr <|> Term.attrInstance) ", " >> "] " >> many1 ident
-@[builtinCommandParser] def «export»       := leading_parser "export " >> ident >> "(" >> many1 ident >> ")"
+@[builtinCommandParser] def «export»       := leading_parser "export " >> ident >> " (" >> many1 ident >> ")"
 def openHiding       := leading_parser atomic (ident >> "hiding") >> many1 (checkColGt >> ident)
-def openRenamingItem := leading_parser ident >> unicodeSymbol "→" "->" >> checkColGt >> ident
+def openRenamingItem := leading_parser ident >> unicodeSymbol " → " " -> " >> checkColGt >> ident
 def openRenaming     := leading_parser atomic (ident >> "renaming") >> sepBy1 openRenamingItem ", "
-def openOnly         := leading_parser atomic (ident >> "(") >> many1 ident >> ")"
+def openOnly         := leading_parser atomic (ident >> " (") >> many1 ident >> ")"
 def openSimple       := leading_parser many1 (checkColGt >> ident)
 def openScoped       := leading_parser "scoped " >> many1 (checkColGt >> ident)
 def openDecl         := openHiding <|> openRenaming <|> openOnly <|> openSimple <|> openScoped