fix(library/init/lean/parser/term): placeholder binder after bracketed binder

2018-11-15 16:02:31 +01:00 · 2018-11-15 16:02:31 +01:00 · d10ff29bea
commit d10ff29bea
parent cd287629cb
1 changed files with 1 additions and 1 deletions
--- 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,
    }+,
  }?
 ]