diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean
index 1f0d5dc33d..685767706f 100644
--- a/src/Lean/Parser/Command.lean
+++ b/src/Lean/Parser/Command.lean
@@ -80,6 +80,7 @@ declModifiers >> («abbrev» <|> «def» <|> «theorem» <|> «constant» <|> «
 @[builtinCommandParser] def «universes»    := parser! "universes " >> many1 ident
 @[builtinCommandParser] def check          := parser! "#check " >> termParser
 @[builtinCommandParser] def check_failure  := parser! "#check_failure " >> termParser -- Like `#check`, but succeeds only if term does not type check
+@[builtinCommandParser] def eval           := parser! "#eval " >> termParser
 @[builtinCommandParser] def synth          := parser! "#synth " >> termParser
 @[builtinCommandParser] def exit           := parser! "#exit"
 @[builtinCommandParser] def «resolve_name» := parser! "#resolve_name " >> ident