diff --git a/library/data/subtype.lean b/library/data/subtype.lean
index ba08528931..ead0377938 100644
--- a/library/data/subtype.lean
+++ b/library/data/subtype.lean
@@ -9,7 +9,7 @@ open decidable
 structure subtype {A : Type} (P : A → Prop) :=
 tag :: (elt_of : A) (has_property : P elt_of)
 
-notation `{` binders `|` r:(scoped 1 P, subtype P) `}` := r
+notation `{` binders:55 `|` r:(scoped 1 P, subtype P) `}` := r
 
 namespace subtype
   variables {A : Type} {P : A → Prop}
diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp
index 3f33bdad3d..0929d5088c 100644
--- a/src/frontends/lean/builtin_exprs.cpp
+++ b/src/frontends/lean/builtin_exprs.cpp
@@ -87,7 +87,8 @@ static expr parse_let(parser & p, pos_info const & pos) {
         } else {
             parser::local_scope scope2(p);
             buffer<expr> ps;
-            auto lenv = p.parse_binders(ps);
+            unsigned rbp = 0;
+            auto lenv = p.parse_binders(ps, rbp);
             if (p.curr_is_token(get_colon_tk())) {
                 p.next();
                 type  = p.parse_scoped_expr(ps, lenv);
@@ -333,7 +334,8 @@ static expr parse_obtain(parser & p, unsigned, expr const *, pos_info const & po
     // exists_elim {A : Type} {P : A → Prop} {B : Prop} (H1 : ∃ x : A, P x) (H2 : ∀ (a : A) (H : P a), B)
     buffer<expr> ps;
     auto b_pos = p.pos();
-    environment env = p.parse_binders(ps);
+    unsigned rbp = 0;
+    environment env = p.parse_binders(ps, rbp);
     unsigned num_ps = ps.size();
     if (num_ps < 2)
         throw parser_error("invalid 'obtain' expression, at least 2 binders expected", b_pos);
diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp
index 5171f86810..6219912539 100644
--- a/src/frontends/lean/decl_cmds.cpp
+++ b/src/frontends/lean/decl_cmds.cpp
@@ -179,7 +179,8 @@ static environment variable_cmd_core(parser & p, variable_kind k) {
     expr type;
     if (!p.curr_is_token(get_colon_tk())) {
         buffer<expr> ps;
-        auto lenv = p.parse_binders(ps);
+        unsigned rbp = 0;
+        auto lenv = p.parse_binders(ps, rbp);
         p.check_token_next(get_colon_tk(), "invalid declaration, ':' expected");
         type = p.parse_scoped_expr(ps, lenv);
         type = Pi(ps, type, p);
diff --git a/src/frontends/lean/inductive_cmd.cpp b/src/frontends/lean/inductive_cmd.cpp
index b29bf01027..af8756ef8d 100644
--- a/src/frontends/lean/inductive_cmd.cpp
+++ b/src/frontends/lean/inductive_cmd.cpp
@@ -181,7 +181,8 @@ struct inductive_cmd_fn {
             type = mk_sort(mk_level_placeholder());
         } else if (m_first && !m_p.curr_is_token(get_colon_tk())) {
             lean_assert(m_params.empty());
-            m_p.parse_binders(ps);
+            unsigned rbp = 0;
+            m_p.parse_binders(ps, rbp);
             m_num_params = ps.size();
             if (m_p.curr_is_token(get_colon_tk())) {
                 m_p.next();
diff --git a/src/frontends/lean/notation_cmd.cpp b/src/frontends/lean/notation_cmd.cpp
index 33a52f7cdf..2b99780a8d 100644
--- a/src/frontends/lean/notation_cmd.cpp
+++ b/src/frontends/lean/notation_cmd.cpp
@@ -389,6 +389,15 @@ static optional<pair<action, parse_table>> find_next(optional<parse_table> const
         return optional<pair<action, parse_table>>();
 }
 
+static unsigned parse_binders_rbp(parser & p) {
+    if (p.curr_is_token(get_colon_tk())) {
+        p.next();
+        return parse_precedence(p, "invalid binder/binders, precedence expected");
+    } else {
+        return 0;
+    }
+}
+
 static notation_entry parse_notation_core(parser & p, bool overload, bool reserve, buffer<token_entry> & new_tokens, bool parse_only) {
     buffer<expr>       locals;
     buffer<transition> ts;
@@ -462,10 +471,12 @@ static notation_entry parse_notation_core(parser & p, bool overload, bool reserv
             reserved_pt = optional<parse_table>();
             if (p.curr_is_token_or_id(get_binder_tk())) {
                 p.next();
-                ts.push_back(transition(tk, mk_binder_action()));
+                unsigned rbp = parse_binders_rbp(p);
+                ts.push_back(transition(tk, mk_binder_action(rbp)));
             } else if (p.curr_is_token_or_id(get_binders_tk())) {
                 p.next();
-                ts.push_back(transition(tk, mk_binders_action()));
+                unsigned rbp = parse_binders_rbp(p);
+                ts.push_back(transition(tk, mk_binders_action(rbp)));
             } else if (p.curr_is_identifier()) {
                 unsigned default_prec = get_default_prec(pt, tk);
                 name n   = p.get_name_val();
diff --git a/src/frontends/lean/parse_table.cpp b/src/frontends/lean/parse_table.cpp
index ebc50b4b06..16fdad1869 100644
--- a/src/frontends/lean/parse_table.cpp
+++ b/src/frontends/lean/parse_table.cpp
@@ -80,6 +80,16 @@ struct expr_action_cell : public action_cell {
         expr_action_cell(action_kind::Expr, rbp) {}
 };
 
+struct binder_action_cell : public expr_action_cell {
+    binder_action_cell(unsigned rbp):
+        expr_action_cell(action_kind::Binder, rbp) {}
+};
+
+struct binders_action_cell : public expr_action_cell {
+    binders_action_cell(unsigned rbp):
+        expr_action_cell(action_kind::Binders, rbp) {}
+};
+
 struct exprs_action_cell : public expr_action_cell {
     name           m_token_sep;
     expr           m_rec;
@@ -122,7 +132,8 @@ action & action::operator=(action const & s) { LEAN_COPY_REF(s); }
 action & action::operator=(action && s) { LEAN_MOVE_REF(s); }
 action_kind action::kind() const { return m_ptr->m_kind; }
 expr_action_cell * to_expr_action(action_cell * c) {
-    lean_assert(c->m_kind == action_kind::Expr || c->m_kind == action_kind::Exprs || c->m_kind == action_kind::ScopedExpr);
+    lean_assert(c->m_kind == action_kind::Expr || c->m_kind == action_kind::Exprs || c->m_kind == action_kind::ScopedExpr ||
+                c->m_kind == action_kind::Binder || c->m_kind == action_kind::Binders);
     return static_cast<expr_action_cell*>(c);
 }
 exprs_action_cell * to_exprs_action(action_cell * c) {
@@ -159,14 +170,14 @@ bool action::is_equal(action const & a) const {
     if (kind() != a.kind())
         return false;
     switch (kind()) {
-    case action_kind::Skip: case action_kind::Binder: case action_kind::Binders:
+    case action_kind::Skip:
         return true;
+    case action_kind::Binder: case action_kind::Binders: case action_kind::Expr:
+        return rbp() == a.rbp();
     case action_kind::Ext:
         return m_ptr == a.m_ptr;
     case action_kind::LuaExt:
         return get_lua_fn() == a.get_lua_fn();
-    case action_kind::Expr:
-        return rbp() == a.rbp();
     case action_kind::Exprs:
         return
             rbp() == a.rbp() &&
@@ -184,8 +195,18 @@ bool action::is_equal(action const & a) const {
 void action::display(std::ostream & out) const {
     switch (kind()) {
     case action_kind::Skip:    out << "skip"; break;
-    case action_kind::Binder:  out << "binder"; break;
-    case action_kind::Binders: out << "binders"; break;
+    case action_kind::Binder:
+        if (rbp() != 0)
+            out << "binder:" << rbp();
+        else
+            out << "binder";
+        break;
+    case action_kind::Binders:
+        if (rbp() != 0)
+            out << "binders:" << rbp();
+        else
+            out << "binders";
+        break;
     case action_kind::Ext:     out << "ext"; break;
     case action_kind::LuaExt:  out << "luaext"; break;
     case action_kind::Expr:    out << rbp(); break;
@@ -212,6 +233,8 @@ bool action::is_simple() const {
 void action_cell::dealloc() {
     switch (m_kind) {
     case action_kind::Expr:       delete(to_expr_action(this)); break;
+    case action_kind::Binder:     delete(to_expr_action(this)); break;
+    case action_kind::Binders:    delete(to_expr_action(this)); break;
     case action_kind::Exprs:      delete(to_exprs_action(this)); break;
     case action_kind::ScopedExpr: delete(to_scoped_expr_action(this)); break;
     case action_kind::Ext:        delete(to_ext_action(this)); break;
@@ -221,25 +244,18 @@ void action_cell::dealloc() {
 }
 
 static action * g_skip_action = nullptr;
-static action * g_binder_action = nullptr;
-static action * g_binders_action = nullptr;
-
 action mk_skip_action() { return *g_skip_action; }
-action mk_binder_action() { return *g_binder_action; }
-action mk_binders_action() { return *g_binders_action; }
 
 void initialize_parse_table() {
     g_skip_action    = new action(new action_cell(action_kind::Skip));
-    g_binder_action  = new action(new action_cell(action_kind::Binder));
-    g_binders_action = new action(new action_cell(action_kind::Binders));
 }
 
 void finalize_parse_table() {
-    delete g_binders_action;
-    delete g_binder_action;
     delete g_skip_action;
 }
 
+action mk_binder_action(unsigned rbp) { return action(new binder_action_cell(rbp)); }
+action mk_binders_action(unsigned rbp) { return action(new binders_action_cell(rbp)); }
 action mk_expr_action(unsigned rbp) { return action(new expr_action_cell(rbp)); }
 action mk_exprs_action(name const & sep, expr const & rec, optional<expr> const & ini,
                        optional<name> const & terminator, bool right, unsigned rbp) {
diff --git a/src/frontends/lean/parse_table.h b/src/frontends/lean/parse_table.h
index 5ca90ae947..3fcbf3fdaa 100644
--- a/src/frontends/lean/parse_table.h
+++ b/src/frontends/lean/parse_table.h
@@ -60,6 +60,8 @@ public:
 
     friend void initialize_parse_table();
     friend action mk_expr_action(unsigned rbp);
+    friend action mk_binders_action(unsigned rbp);
+    friend action mk_binder_action(unsigned rbp);
     friend action mk_exprs_action(name const & sep, expr const & rec, optional<expr> const & ini,
                                   optional<name> const & terminator, bool right, unsigned rbp);
     friend action mk_scoped_expr_action(expr const & rec, unsigned rbp, bool lambda);
@@ -91,8 +93,8 @@ action mk_skip_action();
 action mk_expr_action(unsigned rbp = 0);
 action mk_exprs_action(name const & sep, expr const & rec, optional<expr> const & ini, optional<name> const & terminator, bool right,
                        unsigned rbp = 0);
-action mk_binder_action();
-action mk_binders_action();
+action mk_binder_action(unsigned rbp = 0);
+action mk_binders_action(unsigned rbp = 0);
 action mk_scoped_expr_action(expr const & rec, unsigned rbp = 0, bool lambda = true);
 action mk_ext_action_core(parse_fn const & fn);
 action mk_ext_action(parse_fn const & fn);
diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index 2ffe03bfcf..c435f1d01d 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -761,13 +761,13 @@ void parser::parse_close_binder_info(optional<binder_info> const & bi) {
 }
 
 /** \brief Parse <tt>ID ':' expr</tt>, where the expression represents the type of the identifier. */
-expr parser::parse_binder_core(binder_info const & bi) {
+expr parser::parse_binder_core(binder_info const & bi, unsigned rbp) {
     auto p  = pos();
     name id = check_atomic_id_next("invalid binder, atomic identifier expected");
     expr type;
     if (curr_is_token(get_colon_tk())) {
         next();
-        type = parse_expr();
+        type = parse_expr(rbp);
     } else {
         type = save_pos(mk_expr_placeholder(), p);
     }
@@ -775,12 +775,13 @@ expr parser::parse_binder_core(binder_info const & bi) {
     return save_pos(mk_local(id, type, bi), p);
 }
 
-expr parser::parse_binder() {
+expr parser::parse_binder(unsigned rbp) {
     if (curr_is_identifier()) {
-        return parse_binder_core(binder_info());
+        return parse_binder_core(binder_info(), rbp);
     } else {
         binder_info bi = parse_binder_info();
-        auto r = parse_binder_core(bi);
+        rbp = 0;
+        auto r = parse_binder_core(bi, rbp);
         parse_close_binder_info(bi);
         return r;
     }
@@ -790,7 +791,7 @@ expr parser::parse_binder() {
    \brief Parse <tt>ID ... ID ':' expr</tt>, where the expression
    represents the type of the identifiers.
 */
-void parser::parse_binder_block(buffer<expr> & r, binder_info const & bi) {
+void parser::parse_binder_block(buffer<expr> & r, binder_info const & bi, unsigned rbp) {
     buffer<pair<pos_info, name>> names;
     while (curr_is_identifier()) {
         auto p = pos();
@@ -801,7 +802,7 @@ void parser::parse_binder_block(buffer<expr> & r, binder_info const & bi) {
     optional<expr> type;
     if (curr_is_token(get_colon_tk())) {
         next();
-        type = parse_expr();
+        type = parse_expr(rbp);
     }
     for (auto p : names) {
         expr arg_type = type ? *type : save_pos(mk_expr_placeholder(), p.first);
@@ -813,17 +814,18 @@ void parser::parse_binder_block(buffer<expr> & r, binder_info const & bi) {
 }
 
 void parser::parse_binders_core(buffer<expr> & r, buffer<notation_entry> * nentries,
-                                bool & last_block_delimited) {
+                                bool & last_block_delimited, unsigned rbp) {
     while (true) {
         if (curr_is_identifier()) {
-            parse_binder_block(r, binder_info());
+            parse_binder_block(r, binder_info(), rbp);
             last_block_delimited = false;
         } else {
             optional<binder_info> bi = parse_optional_binder_info();
             if (bi) {
+                rbp = 0;
                 last_block_delimited = true;
                 if (!parse_local_notation_decl(nentries))
-                    parse_binder_block(r, *bi);
+                    parse_binder_block(r, *bi, rbp);
                 parse_close_binder_info(bi);
             } else {
                 return;
@@ -833,11 +835,11 @@ void parser::parse_binders_core(buffer<expr> & r, buffer<notation_entry> * nentr
 }
 
 local_environment parser::parse_binders(buffer<expr> & r, buffer<notation_entry> * nentries,
-                                        bool & last_block_delimited, bool allow_empty) {
+                                        bool & last_block_delimited, bool allow_empty, unsigned rbp) {
     flet<environment> save(m_env, m_env); // save environment
     local_expr_decls::mk_scope scope(m_local_decls);
     unsigned old_sz = r.size();
-    parse_binders_core(r, nentries, last_block_delimited);
+    parse_binders_core(r, nentries, last_block_delimited, rbp);
     if (!allow_empty && old_sz == r.size())
         throw_invalid_open_binder(pos());
     return local_environment(m_env);
@@ -941,12 +943,12 @@ expr parser::parse_notation(parse_table t, expr * left) {
         case notation::action_kind::Binder:
             next();
             binder_pos = pos();
-            ps.push_back(parse_binder());
+            ps.push_back(parse_binder(a.rbp()));
             break;
         case notation::action_kind::Binders:
             next();
             binder_pos = pos();
-            lenv = parse_binders(ps);
+            lenv = parse_binders(ps, a.rbp());
             break;
         case notation::action_kind::ScopedExpr: {
             next();
diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h
index 04d80554f3..3eb065f61e 100644
--- a/src/frontends/lean/parser.h
+++ b/src/frontends/lean/parser.h
@@ -182,10 +182,11 @@ class parser {
     expr parse_numeral_expr();
     expr parse_decimal_expr();
     expr parse_string_expr();
-    expr parse_binder_core(binder_info const & bi);
-    void parse_binder_block(buffer<expr> & r, binder_info const & bi);
-    void parse_binders_core(buffer<expr> & r, buffer<notation_entry> * nentries, bool & last_block_delimited);
-    local_environment parse_binders(buffer<expr> & r, buffer<notation_entry> * nentries, bool & last_block_delimited, bool allow_empty = false);
+    expr parse_binder_core(binder_info const & bi, unsigned rbp);
+    void parse_binder_block(buffer<expr> & r, binder_info const & bi, unsigned rbp);
+    void parse_binders_core(buffer<expr> & r, buffer<notation_entry> * nentries, bool & last_block_delimited, unsigned rbp);
+    local_environment parse_binders(buffer<expr> & r, buffer<notation_entry> * nentries, bool & last_block_delimited,
+                                    bool allow_empty, unsigned rbp);
     bool parse_local_notation_decl(buffer<notation_entry> * entries);
 
     friend environment section_cmd(parser & p);
@@ -321,18 +322,22 @@ public:
 
     level parse_level(unsigned rbp = 0);
 
-    expr parse_binder();
+    expr parse_binder(unsigned rbp);
     local_environment parse_binders(buffer<expr> & r, bool & last_block_delimited) {
-        return parse_binders(r, nullptr, last_block_delimited);
+        unsigned rbp = 0; bool allow_empty = false;
+        return parse_binders(r, nullptr, last_block_delimited, allow_empty, rbp);
     }
-    local_environment parse_binders(buffer<expr> & r) {
-        bool tmp; return parse_binders(r, nullptr, tmp);
+    local_environment parse_binders(buffer<expr> & r, unsigned rbp) {
+        bool tmp; bool allow_empty = false;
+        return parse_binders(r, nullptr, tmp, allow_empty, rbp);
     }
     local_environment parse_optional_binders(buffer<expr> & r) {
-        bool tmp; return parse_binders(r, nullptr, tmp, true);
+        bool tmp; bool allow_empty = true; unsigned rbp = 0;
+        return parse_binders(r, nullptr, tmp, allow_empty, rbp);
     }
     local_environment parse_binders(buffer<expr> & r, buffer<notation_entry> & nentries) {
-        bool tmp; return parse_binders(r, &nentries, tmp);
+        bool tmp; bool allow_empty = false; unsigned rbp = 0;
+        return parse_binders(r, &nentries, tmp, allow_empty, rbp);
     }
     optional<binder_info> parse_optional_binder_info();
     binder_info parse_binder_info();
diff --git a/src/frontends/lean/parser_bindings.cpp b/src/frontends/lean/parser_bindings.cpp
index d0e6bdbc39..df34f14f5a 100644
--- a/src/frontends/lean/parser_bindings.cpp
+++ b/src/frontends/lean/parser_bindings.cpp
@@ -78,12 +78,14 @@ static int parse_expr(lua_State * L) { return push_expr(L, gparser.parse_expr(to
 static int parse_led(lua_State * L) { return push_expr(L, gparser.parse_led(to_expr(L, 1))); }
 static int parse_binders(lua_State * L) {
     buffer<expr> ps;
-    auto lenv = gparser.parse_binders(ps);
+    unsigned rbp = 0;
+    auto lenv    = gparser.parse_binders(ps, rbp);
     return push_local_scope_ext(L, lenv, ps);
 }
 static int parse_binder(lua_State * L) {
     buffer<expr> ps;
-    ps.push_back(gparser.parse_binder());
+    unsigned rbp = 0;
+    ps.push_back(gparser.parse_binder(rbp));
     return push_local_scope_ext(L, gparser.env(), ps);
 }
 static int parse_scoped_expr(lua_State * L) {
diff --git a/src/frontends/lean/structure_cmd.cpp b/src/frontends/lean/structure_cmd.cpp
index 6c420af4ba..23d41da499 100644
--- a/src/frontends/lean/structure_cmd.cpp
+++ b/src/frontends/lean/structure_cmd.cpp
@@ -134,8 +134,10 @@ struct structure_cmd_fn {
 
     /** \brief Parse structure parameters */
     void parse_params() {
-        if (!m_p.curr_is_token(get_extends_tk()) && !m_p.curr_is_token(get_assign_tk()) && !m_p.curr_is_token(get_colon_tk()))
-            m_p.parse_binders(m_params);
+        if (!m_p.curr_is_token(get_extends_tk()) && !m_p.curr_is_token(get_assign_tk()) && !m_p.curr_is_token(get_colon_tk())) {
+            unsigned rbp = 0;
+            m_p.parse_binders(m_params, rbp);
+        }
         for (expr const & l : m_params)
             m_p.add_local(l);
     }
diff --git a/tests/lean/run/sub.lean b/tests/lean/run/sub.lean
new file mode 100644
index 0000000000..d4605cc693
--- /dev/null
+++ b/tests/lean/run/sub.lean
@@ -0,0 +1,6 @@
+import data.subtype data.nat
+open nat
+
+notation `{` binders:55 `|` r:(scoped P, subtype P) `}` := r
+check { x : nat | x > 0 }
+check { (x : nat → nat) | true }