diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean
index 8b2db5dd95..2b9c188651 100644
--- a/src/Lean/Parser/Command.lean
+++ b/src/Lean/Parser/Command.lean
@@ -81,7 +81,8 @@ declModifiers >> («abbrev» <|> «def» <|> «theorem» <|> «constant» <|> «
 @[builtinCommandParser] def eval           := parser! "#eval " >> termParser
 @[builtinCommandParser] def synth          := parser! "#synth " >> termParser
 @[builtinCommandParser] def exit           := parser! "#exit"
-@[builtinCommandParser] def print          := parser! "#print" >> (ident <|> strLit)
+@[builtinCommandParser] def print          := parser! "#print " >> (ident <|> strLit)
+@[builtinCommandParser] def printAxioms    := parser! "#print " >> "axioms " >> optional ident
 @[builtinCommandParser] def «resolve_name» := parser! "#resolve_name " >> ident
 @[builtinCommandParser] def «init_quot»    := parser! "init_quot"
 @[builtinCommandParser] def «set_option»   := parser! "set_option " >> ident >> (nonReservedSymbol "true" <|> nonReservedSymbol "false" <|> strLit <|> numLit)