diff --git a/library/init/lean/parser/command.lean b/library/init/lean/parser/command.lean
index eb9d7e8e0f..b7856e1a42 100644
--- a/library/init/lean/parser/command.lean
+++ b/library/init/lean/parser/command.lean
@@ -54,7 +54,7 @@ node! «namespace» ["namespace", name: ident.parser]
 
 @[derive parser.has_tokens]
 def variable.parser : command_parser :=
-node! «variable» ["variable", binder: term.bracketed_binder.parser]
+node! «variable» ["variable", binder: term.binder.parser]
 
 @[derive parser.has_tokens]
 def variables.parser : command_parser :=
diff --git a/library/init/lean/parser/term.lean b/library/init/lean/parser/term.lean
index 680db0801a..0e69d83034 100644
--- a/library/init/lean/parser/term.lean
+++ b/library/init/lean/parser/term.lean
@@ -121,6 +121,13 @@ node_choice! bracketed_binder {
   anonymous_constructor: anonymous_constructor.parser,
 }
 
+@[derive has_tokens has_view]
+def binder.parser : term_parser :=
+node_choice! binder {
+  bracketed: bracketed_binder.parser,
+  unbracketed: binder_content.parser,
+}
+
 @[derive has_tokens has_view]
 def binders.parser : term_parser :=
 node! binders [