diff --git a/src/kernel/abstract_type_context.cpp b/src/kernel/abstract_type_context.cpp
index 6bbdc869bb..6695c6dbab 100644
--- a/src/kernel/abstract_type_context.cpp
+++ b/src/kernel/abstract_type_context.cpp
@@ -17,10 +17,6 @@ void abstract_type_context::pop_local() {
     /* do nothing */
 }
 
-expr abstract_type_context::abstract(expr const & e, unsigned num_locals, expr const * locals) {
-    return ::lean::abstract(e, num_locals, locals);
-}
-
 push_local_fn::~push_local_fn() {
     for (unsigned i = 0; i < m_counter; i++)
         m_ctx.pop_local();
diff --git a/src/kernel/abstract_type_context.h b/src/kernel/abstract_type_context.h
index dc7c62c210..eff7da93ec 100644
--- a/src/kernel/abstract_type_context.h
+++ b/src/kernel/abstract_type_context.h
@@ -31,7 +31,6 @@ public:
 
     virtual expr push_local(name const & pp_name, expr const & type, binder_info const & bi = binder_info());
     virtual void pop_local();
-    virtual expr abstract(expr const & e, unsigned num_locals, expr const * locals);
 
     expr check(expr const & e, bool infer_only) { return infer_only ? infer(e) : check(e); }
 
diff --git a/src/library/metavar_context.cpp b/src/library/metavar_context.cpp
index 2db5dfb7fe..264848e6ad 100644
--- a/src/library/metavar_context.cpp
+++ b/src/library/metavar_context.cpp
@@ -153,14 +153,14 @@ struct metavar_context::interface_impl {
             m_ctx.m_dassignment.erase(mlocal_name(e));
             buffer<expr> locals;
             to_buffer(d->m_locals, locals);
-            new_v = ::lean::abstract(new_v, locals.size(), locals.data());
+            new_v = abstract(new_v, locals.size(), locals.data());
             unsigned i = locals.size();
             while (i > 0) {
                 --i;
                 local_decl decl = d->m_lctx.get_local_decl(locals[i]);
-                expr type       = ::lean::abstract(decl.get_type(), i, locals.data());
+                expr type       = abstract(decl.get_type(), i, locals.data());
                 if (optional<expr> letval = decl.get_value()) {
-                    letval = ::lean::abstract(*letval, i, locals.data());
+                    letval = abstract(*letval, i, locals.data());
                     new_v  = mk_let(decl.get_user_name(), type, *letval, new_v);
                 } else {
                     new_v  = mk_lambda(decl.get_user_name(), type, new_v, decl.get_info());
diff --git a/src/library/normalize.cpp b/src/library/normalize.cpp
index fc69a1e41e..631a6c324f 100644
--- a/src/library/normalize.cpp
+++ b/src/library/normalize.cpp
@@ -32,7 +32,7 @@ class normalize_fn {
     expr normalize_binding(expr const & e) {
         expr d = normalize(binding_domain(e));
         expr l = m_ctx.push_local(binding_name(e), d, binding_info(e));
-        expr b = m_ctx.abstract(normalize(instantiate(binding_body(e), l)), 1, &l);
+        expr b = abstract(normalize(instantiate(binding_body(e), l)), 1, &l);
         m_ctx.pop_local();
         return update_binding(e, d, b);
     }
diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp
index 9993395f09..7cadf2820c 100644
--- a/src/library/type_context.cpp
+++ b/src/library/type_context.cpp
@@ -417,13 +417,13 @@ expr type_context_old::mk_binding(bool is_pi, local_context const & lctx, unsign
     for (unsigned i = 0; i < num_locals; i++) {
         local_decl decl = lctx.get_local_decl(locals[i]);
         decls.push_back(decl);
-        types.push_back(::lean::abstract(elim_mvar_deps(decl.get_type(), i, locals), i, locals));
+        types.push_back(abstract(elim_mvar_deps(decl.get_type(), i, locals), i, locals));
         if (auto v = decl.get_value())
-            values.push_back(some_expr(::lean::abstract(elim_mvar_deps(*v, i, locals), i, locals)));
+            values.push_back(some_expr(abstract(elim_mvar_deps(*v, i, locals), i, locals)));
         else
             values.push_back(none_expr());
     }
-    expr new_e = ::lean::abstract(elim_mvar_deps(e, num_locals, locals), num_locals, locals);
+    expr new_e = abstract(elim_mvar_deps(e, num_locals, locals), num_locals, locals);
     lean_assert(types.size() == values.size());
     unsigned i = types.size();
     while (i > 0) {
@@ -1103,7 +1103,7 @@ expr type_context_old::infer_lambda(expr e) {
     }
     check_system("infer_type");
     expr t = infer_core(instantiate_rev(e, ls.size(), ls.data()));
-    expr r = ::lean::abstract(t, ls.size(), ls.data());
+    expr r = abstract(t, ls.size(), ls.data());
     unsigned i = es.size();
     while (i > 0) {
         --i;