diff --git a/src/frontends/lean/parser_config.cpp b/src/frontends/lean/parser_config.cpp
index f87204aedd..bdf02f64c2 100644
--- a/src/frontends/lean/parser_config.cpp
+++ b/src/frontends/lean/parser_config.cpp
@@ -346,28 +346,6 @@ environment add_notation(environment const & env, notation_entry const & e, bool
     return notation_ext::add_entry(env, get_dummy_ios(), e, persistent);
 }
 
-environment add_nud_notation(environment const & env, unsigned num, notation::transition const * ts,
-                             expr const & a, bool overload, notation_entry_group g, bool parse_only) {
-    return add_notation(env, notation_entry(true, to_list(ts, ts+num), a, overload, g, parse_only));
-}
-
-environment add_led_notation(environment const & env, unsigned num, notation::transition const * ts,
-                             expr const & a, bool overload, notation_entry_group g, bool parse_only) {
-    return add_notation(env, notation_entry(false, to_list(ts, ts+num), a, overload, g, parse_only));
-}
-
-environment add_nud_notation(environment const & env, std::initializer_list<notation::transition> const & ts,
-                             expr const & a, bool overload, bool parse_only) {
-    notation_entry_group g = notation_entry_group::Main;
-    return add_nud_notation(env, ts.size(), ts.begin(), a, overload, g, parse_only);
-}
-
-environment add_led_notation(environment const & env, std::initializer_list<notation::transition> const & ts,
-                             expr const & a, bool overload, bool parse_only) {
-    notation_entry_group g = notation_entry_group::Main;
-    return add_led_notation(env, ts.size(), ts.begin(), a, overload, g, parse_only);
-}
-
 parse_table const & get_nud_table(environment const & env) {
     return notation_ext::get_state(env).m_nud;
 }
diff --git a/src/frontends/lean/parser_config.h b/src/frontends/lean/parser_config.h
index 34267eff18..fe5bcec89d 100644
--- a/src/frontends/lean/parser_config.h
+++ b/src/frontends/lean/parser_config.h
@@ -67,15 +67,6 @@ environment add_notation(environment const & env, notation_entry const & e, bool
 
 environment add_expr_token(environment const & env, char const * val, unsigned prec);
 environment add_tactic_token(environment const & env, char const * val, unsigned prec);
-
-environment add_nud_notation(environment const & env, unsigned num, notation::transition const * ts, expr const & a,
-                             bool overload = true, notation_entry_group g = notation_entry_group::Main, bool parse_only = false);
-environment add_led_notation(environment const & env, unsigned num, notation::transition const * ts, expr const & a,
-                             bool overload = true, notation_entry_group g = notation_entry_group::Main, bool parse_only = false);
-environment add_nud_notation(environment const & env, std::initializer_list<notation::transition> const & ts, expr const & a,
-                             bool overload = true, bool parse_only = false);
-environment add_led_notation(environment const & env, std::initializer_list<notation::transition> const & ts, expr const & a,
-                             bool overload = true, bool parse_only = false);
 token_table const & get_token_table(environment const & env);
 parse_table const & get_nud_table(environment const & env);
 parse_table const & get_led_table(environment const & env);