diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp
index d3b943f158..c85748e4f0 100644
--- a/src/frontends/lean/builtin_exprs.cpp
+++ b/src/frontends/lean/builtin_exprs.cpp
@@ -428,7 +428,7 @@ static expr parse_overwrite_notation(parser & p, unsigned, expr const *, pos_inf
 }
 
 static expr parse_explicit_expr(parser & p, unsigned, expr const *, pos_info const & pos) {
-    expr e = p.parse_expr(get_max_prec());
+    expr e = p.parse_expr(get_Max_prec());
     if (is_choice(e)) {
         buffer<expr> new_choices;
         for (unsigned i = 0; i < get_num_choices(e); i++)
@@ -440,7 +440,7 @@ static expr parse_explicit_expr(parser & p, unsigned, expr const *, pos_info con
 }
 
 static expr parse_consume_args_expr(parser & p, unsigned, expr const *, pos_info const & pos) {
-    expr e = p.parse_expr(get_max_prec());
+    expr e = p.parse_expr(get_Max_prec());
     if (is_choice(e)) {
         buffer<expr> new_choices;
         for (unsigned i = 0; i < get_num_choices(e); i++)
diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp
index 58d9784e6f..09eb8a9cdb 100644
--- a/src/frontends/lean/token_table.cpp
+++ b/src/frontends/lean/token_table.cpp
@@ -13,9 +13,11 @@ namespace lean {
 static unsigned g_arrow_prec      = 25;
 static unsigned g_decreasing_prec = 100;
 static unsigned g_max_prec        = 1024;
+static unsigned g_Max_prec        = 1024*1024;
 static unsigned g_plus_prec       = 65;
 static unsigned g_cup_prec        = 60;
 unsigned get_max_prec() { return g_max_prec; }
+unsigned get_Max_prec() { return g_Max_prec; }
 unsigned get_arrow_prec() { return g_arrow_prec; }
 unsigned get_decreasing_prec() { return g_decreasing_prec; }
 token_table add_command_token(token_table const & s, char const * token) {
diff --git a/src/frontends/lean/token_table.h b/src/frontends/lean/token_table.h
index 10f0beb3c9..c32928bf1e 100644
--- a/src/frontends/lean/token_table.h
+++ b/src/frontends/lean/token_table.h
@@ -16,7 +16,10 @@ Author: Leonardo de Moura
 #endif
 
 namespace lean {
+// User-level maximum precedence
 unsigned get_max_prec();
+// Internal maximum precedence used for @ and ! operators
+unsigned get_Max_prec();
 unsigned get_arrow_prec();
 unsigned get_decreasing_prec();
 class token_info {
diff --git a/tests/lean/run/prec_max.lean b/tests/lean/run/prec_max.lean
new file mode 100644
index 0000000000..30f6942ed0
--- /dev/null
+++ b/tests/lean/run/prec_max.lean
@@ -0,0 +1,18 @@
+open nat
+
+reserve postfix ⁻¹:(max + 1)
+
+postfix ⁻¹ := eq.symm
+
+constant foo (a b : nat) : a + b = 0
+
+theorem tst1 (a b : nat) : 0 = a + b :=
+!foo⁻¹
+
+constant f {a b : nat} (h1 : 0 = a + b) (h2 : a = b) : a = 0 ∧ b = 0
+
+example (a b : nat) : a = 0 ∧ b = 0 :=
+f !foo⁻¹ sorry
+
+example (a b : nat) : a = 0 ∧ b = 0 :=
+f !foo⁻¹ sorry⁻¹