diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean
index 39bb93d83d..b961814d06 100644
--- a/src/Lean/Parser/Command.lean
+++ b/src/Lean/Parser/Command.lean
@@ -97,6 +97,8 @@ def openSimple       := parser! many1 ident
 
 @[builtinCommandParser] def «mutual» := parser! "mutual " >> many1 (notFollowedBy «end» >> commandParser) >> "end"
 
+@[builtinCommandParser] def «in»  := tparser! " in " >> commandParser
+
 end Command
 end Parser
 end Lean