diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp
index a6532326ad..fbc7804c6b 100644
--- a/src/frontends/lean/builtin_exprs.cpp
+++ b/src/frontends/lean/builtin_exprs.cpp
@@ -793,7 +793,7 @@ static expr parse_parser(parser & p, bool leading, pos_info const & pos) {
         p.check_token_next(get_rbracket_tk(), "`]` expected");
     }
     expr e = p.parse_expr();
-    name n = leading ? get_lean_parser_leading_node_prec_name() : get_lean_parser_trailing_node_prec_name();
+    name n = leading ? get_lean_parser_leading_node_name() : get_lean_parser_trailing_node_name();
     expr r = mk_app(mk_constant(n), quote(kind), prec, e);
     if (leading && kind.is_string()) {
         r = mk_app(mk_constant({"Lean", "Parser", "withAntiquot"}),
diff --git a/src/library/constants.cpp b/src/library/constants.cpp
index 4bfd47b3d2..b80ebab004 100644
--- a/src/library/constants.cpp
+++ b/src/library/constants.cpp
@@ -124,8 +124,6 @@ name const * g_lean_mk_name_num = nullptr;
 name const * g_lean_mk_name_str = nullptr;
 name const * g_lean_parser_leading_node = nullptr;
 name const * g_lean_parser_trailing_node = nullptr;
-name const * g_lean_parser_leading_node_prec = nullptr;
-name const * g_lean_parser_trailing_node_prec = nullptr;
 name const * g_mut_quot = nullptr;
 name const * g_nat = nullptr;
 name const * g_nat_succ = nullptr;
@@ -318,8 +316,6 @@ void initialize_constants() {
     g_lean_mk_name_str = new name{"Lean", "mkNameStr"};
     g_lean_parser_leading_node = new name{"Lean", "Parser", "leadingNode"};
     g_lean_parser_trailing_node = new name{"Lean", "Parser", "trailingNode"};
-    g_lean_parser_leading_node_prec = new name{"Lean", "Parser", "leadingNodePrec"};
-    g_lean_parser_trailing_node_prec = new name{"Lean", "Parser", "trailingNodePrec"};
     g_mut_quot = new name{"MutQuot"};
     g_nat = new name{"Nat"};
     g_nat_succ = new name{"Nat", "succ"};
@@ -513,8 +509,6 @@ void finalize_constants() {
     delete g_lean_mk_name_str;
     delete g_lean_parser_leading_node;
     delete g_lean_parser_trailing_node;
-    delete g_lean_parser_leading_node_prec;
-    delete g_lean_parser_trailing_node_prec;
     delete g_mut_quot;
     delete g_nat;
     delete g_nat_succ;
@@ -707,8 +701,6 @@ name const & get_lean_mk_name_num_name() { return *g_lean_mk_name_num; }
 name const & get_lean_mk_name_str_name() { return *g_lean_mk_name_str; }
 name const & get_lean_parser_leading_node_name() { return *g_lean_parser_leading_node; }
 name const & get_lean_parser_trailing_node_name() { return *g_lean_parser_trailing_node; }
-name const & get_lean_parser_leading_node_prec_name() { return *g_lean_parser_leading_node_prec; }
-name const & get_lean_parser_trailing_node_prec_name() { return *g_lean_parser_trailing_node_prec; }
 name const & get_mut_quot_name() { return *g_mut_quot; }
 name const & get_nat_name() { return *g_nat; }
 name const & get_nat_succ_name() { return *g_nat_succ; }
diff --git a/src/library/constants.h b/src/library/constants.h
index 97fefbf15f..9bb8e4ce91 100644
--- a/src/library/constants.h
+++ b/src/library/constants.h
@@ -126,8 +126,6 @@ name const & get_lean_mk_name_num_name();
 name const & get_lean_mk_name_str_name();
 name const & get_lean_parser_leading_node_name();
 name const & get_lean_parser_trailing_node_name();
-name const & get_lean_parser_leading_node_prec_name();
-name const & get_lean_parser_trailing_node_prec_name();
 name const & get_mut_quot_name();
 name const & get_nat_name();
 name const & get_nat_succ_name();
diff --git a/src/library/constants.txt b/src/library/constants.txt
index 4e21908e5a..191c4b85e9 100644
--- a/src/library/constants.txt
+++ b/src/library/constants.txt
@@ -119,8 +119,6 @@ Lean.mkNameNum
 Lean.mkNameStr
 Lean.Parser.leadingNode
 Lean.Parser.trailingNode
-Lean.Parser.leadingNodePrec
-Lean.Parser.trailingNodePrec
 MutQuot
 Nat
 Nat.succ
diff --git a/stage0/src/frontends/lean/builtin_exprs.cpp b/stage0/src/frontends/lean/builtin_exprs.cpp
index a6532326ad..fbc7804c6b 100644
--- a/stage0/src/frontends/lean/builtin_exprs.cpp
+++ b/stage0/src/frontends/lean/builtin_exprs.cpp
@@ -793,7 +793,7 @@ static expr parse_parser(parser & p, bool leading, pos_info const & pos) {
         p.check_token_next(get_rbracket_tk(), "`]` expected");
     }
     expr e = p.parse_expr();
-    name n = leading ? get_lean_parser_leading_node_prec_name() : get_lean_parser_trailing_node_prec_name();
+    name n = leading ? get_lean_parser_leading_node_name() : get_lean_parser_trailing_node_name();
     expr r = mk_app(mk_constant(n), quote(kind), prec, e);
     if (leading && kind.is_string()) {
         r = mk_app(mk_constant({"Lean", "Parser", "withAntiquot"}),
diff --git a/stage0/src/library/constants.cpp b/stage0/src/library/constants.cpp
index 4bfd47b3d2..b80ebab004 100644
--- a/stage0/src/library/constants.cpp
+++ b/stage0/src/library/constants.cpp
@@ -124,8 +124,6 @@ name const * g_lean_mk_name_num = nullptr;
 name const * g_lean_mk_name_str = nullptr;
 name const * g_lean_parser_leading_node = nullptr;
 name const * g_lean_parser_trailing_node = nullptr;
-name const * g_lean_parser_leading_node_prec = nullptr;
-name const * g_lean_parser_trailing_node_prec = nullptr;
 name const * g_mut_quot = nullptr;
 name const * g_nat = nullptr;
 name const * g_nat_succ = nullptr;
@@ -318,8 +316,6 @@ void initialize_constants() {
     g_lean_mk_name_str = new name{"Lean", "mkNameStr"};
     g_lean_parser_leading_node = new name{"Lean", "Parser", "leadingNode"};
     g_lean_parser_trailing_node = new name{"Lean", "Parser", "trailingNode"};
-    g_lean_parser_leading_node_prec = new name{"Lean", "Parser", "leadingNodePrec"};
-    g_lean_parser_trailing_node_prec = new name{"Lean", "Parser", "trailingNodePrec"};
     g_mut_quot = new name{"MutQuot"};
     g_nat = new name{"Nat"};
     g_nat_succ = new name{"Nat", "succ"};
@@ -513,8 +509,6 @@ void finalize_constants() {
     delete g_lean_mk_name_str;
     delete g_lean_parser_leading_node;
     delete g_lean_parser_trailing_node;
-    delete g_lean_parser_leading_node_prec;
-    delete g_lean_parser_trailing_node_prec;
     delete g_mut_quot;
     delete g_nat;
     delete g_nat_succ;
@@ -707,8 +701,6 @@ name const & get_lean_mk_name_num_name() { return *g_lean_mk_name_num; }
 name const & get_lean_mk_name_str_name() { return *g_lean_mk_name_str; }
 name const & get_lean_parser_leading_node_name() { return *g_lean_parser_leading_node; }
 name const & get_lean_parser_trailing_node_name() { return *g_lean_parser_trailing_node; }
-name const & get_lean_parser_leading_node_prec_name() { return *g_lean_parser_leading_node_prec; }
-name const & get_lean_parser_trailing_node_prec_name() { return *g_lean_parser_trailing_node_prec; }
 name const & get_mut_quot_name() { return *g_mut_quot; }
 name const & get_nat_name() { return *g_nat; }
 name const & get_nat_succ_name() { return *g_nat_succ; }
diff --git a/stage0/src/library/constants.h b/stage0/src/library/constants.h
index 97fefbf15f..9bb8e4ce91 100644
--- a/stage0/src/library/constants.h
+++ b/stage0/src/library/constants.h
@@ -126,8 +126,6 @@ name const & get_lean_mk_name_num_name();
 name const & get_lean_mk_name_str_name();
 name const & get_lean_parser_leading_node_name();
 name const & get_lean_parser_trailing_node_name();
-name const & get_lean_parser_leading_node_prec_name();
-name const & get_lean_parser_trailing_node_prec_name();
 name const & get_mut_quot_name();
 name const & get_nat_name();
 name const & get_nat_succ_name();
diff --git a/stage0/src/library/constants.txt b/stage0/src/library/constants.txt
index 4e21908e5a..191c4b85e9 100644
--- a/stage0/src/library/constants.txt
+++ b/stage0/src/library/constants.txt
@@ -119,8 +119,6 @@ Lean.mkNameNum
 Lean.mkNameStr
 Lean.Parser.leadingNode
 Lean.Parser.trailingNode
-Lean.Parser.leadingNodePrec
-Lean.Parser.trailingNodePrec
 MutQuot
 Nat
 Nat.succ