diff --git a/library/init/lean/parser/term.lean b/library/init/lean/parser/term.lean
index 8d7f835631..23fc19f1ca 100644
--- a/library/init/lean/parser/term.lean
+++ b/library/init/lean/parser/term.lean
@@ -133,7 +133,7 @@ node! binders [
     -- we allow mixing like in `a (b : β) c`, but not `a : α (b : β) c : γ`
     mixed: node_choice! mixed_binder {
       bracketed: bracketed_binder.parser,
-      id: ident.parser,
+      id: binder_ident.parser,
     }+,
   }?
 ]