diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp
index 92fbf5b6d3..7e75313779 100644
--- a/src/frontends/lean/builtin_cmds.cpp
+++ b/src/frontends/lean/builtin_cmds.cpp
@@ -110,16 +110,13 @@ static environment redeclare_aliases(environment env, parser & p,
     if (!in_section(old_env))
         return env;
     list<pair<name, expr>> new_entries = p.get_local_entries();
-    buffer<pair<name, expr>> to_redeclare;
     unsigned new_len = length(new_entries);
     unsigned old_len = length(old_entries);
     lean_assert(old_len >= new_len);
     name_set popped_locals;
     while (old_len > new_len) {
         pair<name, expr> entry = head(old_entries);
-        if (is_local_ref(entry.second))
-            to_redeclare.push_back(entry);
-        else if (is_local_p(entry.second))
+        if (is_local_p(entry.second))
             popped_locals.insert(local_name_p(entry.second));
         old_entries = tail(old_entries);
         old_len--;
@@ -130,11 +127,6 @@ static environment redeclare_aliases(environment env, parser & p,
             if (is_param(l) && !is_placeholder(l) && !level_decls.contains(n))
                 popped_levels.insert(param_id(l));
         });
-    for (auto const & entry : to_redeclare) {
-        expr new_ref = update_local_ref(entry.second, popped_levels, popped_locals);
-        if (!is_constant(new_ref))
-            env = p.add_local_ref(env, entry.first, new_ref);
-    }
     return env;
 }
 
diff --git a/src/frontends/lean/decl_util.cpp b/src/frontends/lean/decl_util.cpp
index 2a9e38a510..f9cee32320 100644
--- a/src/frontends/lean/decl_util.cpp
+++ b/src/frontends/lean/decl_util.cpp
@@ -333,56 +333,6 @@ void elaborate_params(elaborator & elab, buffer<expr> const & params, buffer<exp
     }
 }
 
-environment add_local_ref(parser & p, environment const & env, name const & c_name, name const & c_real_name, buffer<name> const & lp_names, buffer<expr> const & var_params) {
-    buffer<expr> params;
-    buffer<name> lps;
-    for (name const & u : lp_names) {
-        if (!p.is_local_level(u)) {
-            /* Stop, it is a definition parameter */
-            break;
-        } else if (p.is_local_level_variable(u)) {
-            /* Stop, it is a parser universe variable (i.e., it has been declared using the `universe variable` command */
-            break;
-        } else {
-            lps.push_back(u);
-        }
-    }
-    for (expr const & e : var_params) {
-        if (!p.is_local_decl(e)) {
-            /* Stop, it is a definition parameter */
-            break;
-        } else if (p.is_local_variable(e)) {
-            /* Stop, it is a parser variable (i.e., it has been declared using the `variable` command */
-            break;
-        } else {
-            /* It is a parser parameter (i.e., it has been declared with the `parameter` command */
-            params.push_back(e);
-        }
-    }
-    if (lps.empty() && params.empty()) return env;
-    /*
-      Procedures such as `collect_implicit_locals` wrap parameter types with the `as_is` annotation.
-      So, we remove these annotations before creating the local reference using `mk_local_ref`.
-      Remark: the resulting object is wrapped with the macro `as_atomic`.
-
-      Remark: The local constants created here and `collect_implicit_locals` are not structurally
-      equal. That is, `l : ty` is not structurally equal to `l : as_is ty`, but they are definitionally
-      equal, and moreover the collection method relies on the fact that they have the same internal
-      id.
-    */
-    buffer<expr> new_params;
-    for (unsigned i = 0; i < params.size(); i++) {
-        expr & param = params[i];
-        expr type          = local_type_p(param);
-        if (is_as_is(type))
-            type = get_as_is_arg(type);
-        expr new_type      = replace_locals_preserving_pos_info(type, i, params.data(), new_params.data());
-        new_params.push_back(copy_pos(param, update_local_p(param, new_type)));
-    }
-    expr ref = mk_local_ref(c_real_name, lparams_to_levels(names(lps)), new_params);
-    return p.add_local_ref(env, c_name, ref);
-}
-
 environment add_alias(environment const & env, bool is_protected, name const & c_name, name const & c_real_name) {
     if (c_name != c_real_name) {
         if (is_protected)
diff --git a/src/frontends/lean/decl_util.h b/src/frontends/lean/decl_util.h
index 74eea709ce..b221945c33 100644
--- a/src/frontends/lean/decl_util.h
+++ b/src/frontends/lean/decl_util.h
@@ -173,8 +173,6 @@ void elaborate_params(elaborator & elab, buffer<expr> const & params, buffer<exp
 /** \brief Create an alias c_name --> (c_real_name.{level_params} params)
     level_params and params are subsets of lp_names and var_params that were
     declared using the parameter command. */
-environment add_local_ref(parser & p, environment const & env, name const & c_name, name const & c_real_name,
-                          buffer<name> const & lp_names, buffer<expr> const & var_params);
 
 /** \brief Add alias for new declaration. */
 environment add_alias(environment const & env, bool is_protected, name const & c_name, name const & c_real_name);
diff --git a/src/frontends/lean/definition_cmds.cpp b/src/frontends/lean/definition_cmds.cpp
index 8116bc1971..080bfa3fcd 100644
--- a/src/frontends/lean/definition_cmds.cpp
+++ b/src/frontends/lean/definition_cmds.cpp
@@ -259,7 +259,6 @@ static environment elab_defs_core(parser & p, decl_cmd_kind kind, cmd_meta const
         name c_real_name;
         std::tie(env, c_real_name) = declare_definition(env, kind, lp_names, c_name, prv_names[i],
                                                         curr_type, some_expr(curr), meta);
-        env = add_local_ref(p, env, c_name, c_real_name, lp_names, params);
         new_d_names.push_back(c_real_name);
         elab.set_env(env);
     }
@@ -566,7 +565,6 @@ static environment elab_single_def(parser & p, decl_cmd_kind const & kind, cmd_m
         time_task _("decl post-processing", p.mk_message(header_pos, INFORMATION), c_name);
         environment new_env = env_n.first;
         name c_real_name    = env_n.second;
-        new_env = add_local_ref(p, new_env, c_name, c_real_name, lp_names, params);
         if (!meta.m_modifiers.m_is_unsafe && !meta.m_modifiers.m_is_partial &&
             (kind == decl_cmd_kind::Definition || kind == decl_cmd_kind::Instance)) {
             new_env = mk_smart_unfolding_definition(new_env, p.get_options(), c_real_name);
diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index 6767d4b901..7c39d02e33 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -385,25 +385,6 @@ void parser::add_local_expr(name const & n, expr const & p, bool is_variable) {
     }
 }
 
-environment parser::add_local_ref(environment const & env, name const & n, expr const & ref) {
-    add_local_expr(n, ref, false);
-    if (is_as_atomic(ref)) {
-        buffer<expr> args;
-        expr f = get_app_args(get_as_atomic_arg(ref), args);
-        if (is_explicit(f))
-            f = get_explicit_arg(f);
-        if (is_constant(f)) {
-            return ::lean::add_local_ref(env, const_name(f), ref);
-        } else {
-            return env;
-        }
-    } else if (is_constant(ref) && const_levels(ref)) {
-        return ::lean::add_local_ref(env, const_name(ref), ref);
-    } else {
-        return env;
-    }
-}
-
 static void check_no_metavars(name const & n, expr const & e) {
     lean_assert(is_local_p(e));
     if (has_metavar(e)) {
@@ -1750,11 +1731,6 @@ expr parser::id_to_expr(name const & id, pos_info const & p, bool resolve_only,
         return save_pos(mk_local(id, save_pos(mk_expr_placeholder(), p)), p);
     }
 
-    if (auto ref = get_local_ref(m_env, id)) {
-        check_no_levels(ls, p);
-        return copy_with_new_pos(*ref, p);
-    }
-
     for (name const & ns : get_namespaces(m_env)) {
         auto new_id = ns + id;
         if (!ns.is_anonymous() && m_env.find(new_id) &&
diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h
index e846155681..f91ccc1edb 100644
--- a/src/frontends/lean/parser.h
+++ b/src/frontends/lean/parser.h
@@ -461,7 +461,6 @@ public:
     bool has_locals() const { return !m_local_decls.empty() || !m_local_level_decls.empty(); }
     void add_local_level(name const & n, level const & l, bool is_variable = false);
     void add_local_expr(name const & n, expr const & p, bool is_variable = false);
-    environment add_local_ref(environment const & env, name const & n, expr const & ref);
     void add_variable(name const & n, expr const & p);
     void add_parameter(name const & n, expr const & p);
     void add_local(expr const & p) { return add_local_expr(local_pp_name_p(p), p); }
diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp
index c926d9dc42..4beb767275 100644
--- a/src/frontends/lean/pp.cpp
+++ b/src/frontends/lean/pp.cpp
@@ -490,94 +490,6 @@ static expr consume_ref_annotations(expr const & e) {
         return e;
 }
 
-enum local_ref_kind { LocalRef, OverridenLocalRef, NotLocalRef };
-
-static local_ref_kind check_local_ref(environment const & env, expr const & e, unsigned & num_ref_univ_params) {
-    expr const & rfn = get_app_fn(e);
-    if (!is_constant(rfn))
-        return NotLocalRef;
-    auto ref = get_local_ref(env, const_name(rfn));
-    if (!ref)
-        return NotLocalRef;
-    if (is_as_atomic(*ref))
-        ref = get_as_atomic_arg(*ref);
-    buffer<expr> ref_args, e_args;
-    expr ref_fn = consume_ref_annotations(get_app_args(*ref, ref_args));
-    get_app_args(e, e_args);
-    if (!is_constant(ref_fn) || e_args.size() != ref_args.size()) {
-        return NotLocalRef;
-    }
-    for (unsigned i = 0; i < e_args.size(); i++) {
-        expr e_arg   = e_args[i];
-        expr ref_arg = consume_ref_annotations(ref_args[i]);
-        if (!is_local(e_arg) || !is_local(ref_arg) || local_pp_name(e_arg) != local_pp_name(ref_arg))
-            return OverridenLocalRef;
-    }
-    num_ref_univ_params = length(const_levels(ref_fn));
-    buffer<level> lvls;
-    to_buffer(const_levels(rfn), lvls);
-    if (lvls.size() < num_ref_univ_params) {
-        return NotLocalRef;
-    }
-    for (unsigned i = 0; i < num_ref_univ_params; i++) {
-        level const & l = lvls[i];
-        if (!is_param(l)) {
-            return OverridenLocalRef;
-        }
-        for (unsigned j = 0; j < i; j++)
-            if (lvls[i] == lvls[j]) {
-                return OverridenLocalRef;
-            }
-    }
-    return LocalRef;
-}
-
-static bool is_local_ref(environment const & env, expr const & e) {
-    unsigned num_ref_univ_params;
-    return check_local_ref(env, e, num_ref_univ_params) == LocalRef;
-}
-
-auto pretty_fn::pp_overriden_local_ref(expr const & e) -> result {
-    buffer<expr> args;
-    expr const & fn = get_app_args(e, args);
-    result res_fn;
-    {
-        flet<bool> set1(m_full_names, true);
-        res_fn = pp_const(fn, some(0u));
-    }
-    format fn_fmt    = res_fn.fmt();
-    if (const_name(fn).is_atomic())
-        fn_fmt = compose(format("_root_."), fn_fmt);
-    if (m_implict && has_implicit_args(fn))
-        fn_fmt = compose(*g_explicit_fmt, fn_fmt);
-    format r_fmt = fn_fmt;
-    expr curr_fn = fn;
-    for (unsigned i = 0; i < args.size(); i++) {
-        expr const & arg = args[i];
-        if (m_implict || !is_implicit(curr_fn)) {
-            result res_arg   = pp_child(arg, max_bp());
-            r_fmt = group(compose(r_fmt, nest(m_indent, compose(line(), res_arg.fmt()))));
-        }
-        curr_fn = mk_app(curr_fn, arg);
-    }
-    return result(max_bp()-1, r_fmt);
-}
-
-// Return some result if \c e is of the form (c p_1 ... p_n) where
-// c is a constant, and p_i's are parameters fixed in a section.
-auto pretty_fn::pp_local_ref(expr const & e) -> optional<result> {
-    unsigned num_ref_univ_params;
-    switch (check_local_ref(m_env, e, num_ref_univ_params)) {
-    case NotLocalRef:
-        return optional<result>();
-    case LocalRef:
-        return some(pp_const(get_app_fn(e), optional<unsigned>(num_ref_univ_params)));
-    case OverridenLocalRef:
-        return some(pp_overriden_local_ref(e));
-    }
-    lean_unreachable();
-}
-
 static bool is_coercion(expr const & e) {
     return is_app_of(e, get_coe_name()) && get_app_num_args(e) >= 4;
 }
@@ -612,8 +524,6 @@ auto pretty_fn::pp_hide_coercion_fn(expr const & e, unsigned bp, bool ignore_hid
 
 auto pretty_fn::pp_child(expr const & e, unsigned bp, bool ignore_hide) -> result {
     if (is_app(e)) {
-        if (auto r = pp_local_ref(e))
-            return add_paren_if_needed(*r, bp);
         if (m_numerals) {
             if (auto n = to_num(e)) return pp_num(*n, bp);
         }
@@ -681,10 +591,6 @@ auto pretty_fn::pp_const(expr const & e, optional<unsigned> const & num_ref_univ
     name n = const_name(e);
     if (m_notation && n == get_unit_unit_name())
         return format("()");
-    if (!num_ref_univ_params) {
-        if (auto r = pp_local_ref(e))
-            return *r;
-    }
     // Remark: if num_ref_univ_params is "some", then it contains the number of
     // universe levels that are fixed in a section. That is, \c e corresponds to
     // a constant in a section which has fixed levels.
@@ -869,8 +775,6 @@ auto pretty_fn::pp_field_notation(expr const & e) -> result {
 }
 
 auto pretty_fn::pp_app(expr const & e) -> result {
-    if (auto r = pp_local_ref(e))
-        return *r;
     if (is_default_arg_app(e))
         return pp_child(app_fn(e), max_bp());
     expr const & fn = app_fn(e);
@@ -885,7 +789,7 @@ auto pretty_fn::pp_app(expr const & e) -> result {
     bool ignore_hide = true;
     result res_fn    = pp_child(fn, max_bp()-1, ignore_hide);
     format fn_fmt    = res_fn.fmt();
-    if (m_implict && (!is_app(fn) || (is_local_ref(m_env, fn))) && has_implicit_args(fn))
+    if (m_implict && !is_app(fn) && has_implicit_args(fn))
         fn_fmt = compose(*g_explicit_fmt, fn_fmt);
     result res_arg = pp_child(app_arg(e), max_bp());
     return result(max_bp()-1, group(compose(fn_fmt, nest(m_indent, compose(line(), res_arg.fmt())))));
diff --git a/src/frontends/lean/pp.h b/src/frontends/lean/pp.h
index 7998a25147..4e08f8095a 100644
--- a/src/frontends/lean/pp.h
+++ b/src/frontends/lean/pp.h
@@ -123,9 +123,6 @@ private:
     result add_paren_if_needed(result const & r, unsigned bp);
     std::pair<bool, token_table const *> needs_space_sep(token_table const * t, std::string const &s1, std::string const &s2) const;
 
-    result pp_overriden_local_ref(expr const & e);
-    optional<result> pp_local_ref(expr const & e);
-
     result pp_hide_coercion(expr const & e, unsigned bp, bool ignore_hide = false);
     result pp_hide_coercion_fn(expr const & e, unsigned bp, bool ignore_hide = false);
     result pp_child_core(expr const & e, unsigned bp, bool ignore_hide = false);
diff --git a/src/frontends/lean/type_util.cpp b/src/frontends/lean/type_util.cpp
index 10be31a71a..3f4748ccf3 100644
--- a/src/frontends/lean/type_util.cpp
+++ b/src/frontends/lean/type_util.cpp
@@ -13,10 +13,10 @@ Author: Leonardo de Moura
 namespace lean {
 environment add_alias(parser & p, environment env, name const & id, name const & full_id,
                       levels const & ctx_levels, buffer<expr> const & ctx_params) {
-    if (!empty(ctx_levels) || !ctx_params.empty()) {
-        expr r = mk_local_ref(full_id, ctx_levels, ctx_params);
-        env = p.add_local_ref(env, id, r);
-    }
+//    if (!empty(ctx_levels) || !ctx_params.empty()) {
+//        expr r = mk_local_ref(full_id, ctx_levels, ctx_params);
+//        env = p.add_local_ref(env, id, r);
+//    }
     if (full_id != id)
         env = add_expr_alias_rec(env, id, full_id);
     return env;
diff --git a/src/library/aliases.cpp b/src/library/aliases.cpp
index 2577264b5f..4ec7201b52 100644
--- a/src/library/aliases.cpp
+++ b/src/library/aliases.cpp
@@ -27,24 +27,15 @@ struct aliases_ext : public environment_extension {
         bool                  m_in_section;
         name_map<names>       m_aliases;
         name_map<name>        m_inv_aliases;
-        name_map<expr>        m_local_refs;
         state():m_in_section(false) {}
 
-        void add_local_ref(name const & a, expr const & ref) {
-            m_local_refs.insert(a, ref);
-        }
-
         void add_expr_alias(name const & a, name const & e, bool overwrite) {
-            if (auto ref = m_local_refs.find(e)) {
-                add_local_ref(a, *ref);
-            } else {
-                auto it = m_aliases.find(a);
-                if (it && !overwrite)
-                    m_aliases.insert(a, cons(e, filter(*it, [&](name const & t) { return t != e; })));
-                else
-                    m_aliases.insert(a, names(e));
-                m_inv_aliases.insert(e, a);
-            }
+            auto it = m_aliases.find(a);
+            if (it && !overwrite)
+                m_aliases.insert(a, cons(e, filter(*it, [&](name const & t) { return t != e; })));
+            else
+                m_aliases.insert(a, names(e));
+            m_inv_aliases.insert(e, a);
         }
     };
 
@@ -76,10 +67,6 @@ struct aliases_ext : public environment_extension {
         add_expr_alias(a, e, overwrite);
     }
 
-    void add_local_ref(name const & a, expr const & ref) {
-        m_state.add_local_ref(a, ref);
-    }
-
     void push(bool in_section) {
         m_scopes = cons(m_state, m_scopes);
         m_state.m_in_section = in_section;
@@ -150,20 +137,6 @@ environment erase_expr_aliases(environment const & env, name const & n) {
     return update(env, ext);
 }
 
-environment add_local_ref(environment const & env, name const & a, expr const & ref) {
-    aliases_ext ext = get_extension(env);
-    ext.add_local_ref(a, ref);
-    return update(env, ext);
-}
-
-optional<expr> get_local_ref(environment const & env, name const & n) {
-    aliases_ext const & ext = get_extension(env);
-    if (auto r = ext.m_state.m_local_refs.find(n))
-        return some_expr(*r);
-    else
-        return none_expr();
-}
-
 // Return true iff \c n is (prefix + ex) for some ex in exceptions
 bool is_exception(name const & n, name const & prefix, unsigned num_exceptions, name const * exceptions) {
     return std::any_of(exceptions, exceptions + num_exceptions, [&](name const & ex) { return (prefix + ex) == n; });
diff --git a/src/library/aliases.h b/src/library/aliases.h
index cf11f59ebc..2257a1952c 100644
--- a/src/library/aliases.h
+++ b/src/library/aliases.h
@@ -42,12 +42,6 @@ bool is_exception(name const & n, name const & prefix, unsigned num_exceptions,
 
 void for_each_expr_alias(environment const & env, std::function<void(name const &, names const &)> const & fn);
 
-/* When we declare a definition in a section, we create an alias for it that fixes the parameters in
-   universe parameters. */
-environment add_local_ref(environment const & env, name const & a, expr const & ref);
-
-optional<expr> get_local_ref(environment const & env, name const & n);
-
 void initialize_aliases();
 void finalize_aliases();
 }