From d10ff29bea134082bc056cd74d7b300b74f7abeb Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Thu, 15 Nov 2018 16:02:31 +0100
Subject: [PATCH] fix(library/init/lean/parser/term): placeholder binder after
 bracketed binder

---
 library/init/lean/parser/term.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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,
     }+,
   }?
 ]