diff --git a/src/library/aliases.cpp b/src/library/aliases.cpp
index 9001cae8f9..cb8a696a56 100644
--- a/src/library/aliases.cpp
+++ b/src/library/aliases.cpp
@@ -95,11 +95,6 @@ struct aliases_ext : public environment_extension {
         return env;
     }
 
-    static environment export_namespace(environment const & env, io_state const &, name const &) {
-        // do nothing, aliases are treated in a special way in the frontend.
-        return env;
-    }
-
     static environment push_scope(environment const & env, io_state const &, scope_kind k) {
         aliases_ext ext = get_extension(env);
         ext.push(k != scope_kind::Namespace);
@@ -119,9 +114,7 @@ static name * g_aliases = nullptr;
 struct aliases_ext_reg {
     unsigned m_ext_id;
     aliases_ext_reg() {
-        register_scoped_ext(*g_aliases,
-                            aliases_ext::using_namespace, aliases_ext::export_namespace,
-                            aliases_ext::push_scope, aliases_ext::pop_scope);
+        register_scoped_ext(*g_aliases, aliases_ext::using_namespace, aliases_ext::push_scope, aliases_ext::pop_scope);
         m_ext_id = environment::register_extension(std::make_shared<aliases_ext>());
     }
 };
diff --git a/src/library/scoped_ext.cpp b/src/library/scoped_ext.cpp
index 25c1bad4e4..47a1a897e4 100644
--- a/src/library/scoped_ext.cpp
+++ b/src/library/scoped_ext.cpp
@@ -11,13 +11,13 @@ Author: Leonardo de Moura
 #include "library/scoped_ext.h"
 
 namespace lean {
-typedef std::tuple<name, using_namespace_fn, export_namespace_fn, push_scope_fn, pop_scope_fn> entry;
+typedef std::tuple<name, using_namespace_fn, push_scope_fn, pop_scope_fn> entry;
 typedef std::vector<entry> scoped_exts;
 static scoped_exts * g_exts = nullptr;
 static scoped_exts & get_exts() { return *g_exts; }
 
-void register_scoped_ext(name const & c, using_namespace_fn use, export_namespace_fn ex, push_scope_fn push, pop_scope_fn pop) {
-    get_exts().emplace_back(c, use, ex, push, pop);
+void register_scoped_ext(name const & c, using_namespace_fn use, push_scope_fn push, pop_scope_fn pop) {
+    get_exts().emplace_back(c, use, push, pop);
 }
 
 struct scope_mng_ext : public environment_extension {
@@ -96,21 +96,6 @@ environment using_namespace(environment const & env, io_state const & ios, name
     return using_namespace(env, ios, n, metaclasses);
 }
 
-environment export_namespace(environment const & env, io_state const & ios, name const & n, buffer<name> const & metaclasses) {
-    environment r = env;
-    for (auto const & t : get_exts()) {
-        if (metaclasses.empty() ||
-            std::find(metaclasses.begin(), metaclasses.end(), std::get<0>(t)) != metaclasses.end())
-            r = std::get<2>(t)(r, ios, n);
-    }
-    return r;
-}
-
-environment export_namespace(environment const & env, io_state const & ios, name const & n) {
-    buffer<name> metaclasses;
-    return export_namespace(env, ios, n, metaclasses);
-}
-
 optional<name> to_valid_namespace_name(environment const & env, name const & n) {
     scope_mng_ext const & ext = get_extension(env);
     if (ext.m_namespace_set.contains(n))
@@ -157,7 +142,7 @@ environment push_scope(environment const & env, io_state const & ios, scope_kind
     ext.m_scope_kinds = cons(k, ext.m_scope_kinds);
     environment r = update(env, ext);
     for (auto const & t : get_exts()) {
-        r = std::get<3>(t)(r, ios, k);
+        r = std::get<2>(t)(r, ios, k);
     }
     if (k == scope_kind::Namespace)
         r = using_namespace(r, ios, new_n);
@@ -188,7 +173,7 @@ environment pop_scope_core(environment const & env, io_state const & ios) {
     ext.m_scope_kinds = tail(ext.m_scope_kinds);
     environment r = update(env, ext);
     for (auto const & t : get_exts()) {
-        r = std::get<4>(t)(r, ios, k);
+        r = std::get<3>(t)(r, ios, k);
     }
     return r;
 }
diff --git a/src/library/scoped_ext.h b/src/library/scoped_ext.h
index af87beaad6..44bd0e037c 100644
--- a/src/library/scoped_ext.h
+++ b/src/library/scoped_ext.h
@@ -17,19 +17,14 @@ Author: Leonardo de Moura
 namespace lean {
 enum class scope_kind { Namespace, Section };
 typedef environment (*using_namespace_fn)(environment const &, io_state const &, name const &);
-typedef environment (*export_namespace_fn)(environment const &, io_state const &, name const &);
 typedef environment (*push_scope_fn)(environment const &, io_state const &, scope_kind);
 typedef environment (*pop_scope_fn)(environment const &, io_state const &, scope_kind);
 
-void register_scoped_ext(name const & n, using_namespace_fn use, export_namespace_fn ex, push_scope_fn push, pop_scope_fn pop);
+void register_scoped_ext(name const & n, using_namespace_fn use, push_scope_fn push, pop_scope_fn pop);
 /** \brief Use objects defined in the namespace \c n.
     If \c metaclasses is not empty, then only objects in the given "metaclasses" \c c are considered. */
 environment using_namespace(environment const & env, io_state const & ios, name const & n, buffer<name> const & metaclasses);
 environment using_namespace(environment const & env, io_state const & ios, name const & n);
-/** \brief Export objects defined in the namespace \c n to current namespace.
-    If \c metaclasses is not empty, then only objects in the given "metaclasses" \c c are considered. */
-environment export_namespace(environment const & env, io_state const & ios, name const & n, buffer<name> const & metaclasses);
-environment export_namespace(environment const & env, io_state const & ios, name const & n);
 
 /** \brief Create a new scope, all scoped extensions are notified. */
 environment push_scope(environment const & env, io_state const & ios, scope_kind k, name const & n = name());
@@ -207,21 +202,6 @@ public:
         return r;
     }
 
-    /** \brief Copy entries from the given namespace to the current namespace. */
-    environment export_namespace(environment env, io_state const & ios, name const & ns) const {
-        if (auto it = m_entries_map.find(ns)) {
-            buffer<entry> entries;
-            to_buffer(*it, entries);
-            unsigned i      = entries.size();
-            name current_ns = get_namespace(env);
-            while (i > 0) {
-                --i;
-                env = add_entry(env, ios, entries[i], current_ns, true);
-            }
-        }
-        return env;
-    }
-
     /** \brief Open a namespace/section. It return the new updated state. */
     scoped_ext push() const {
         scoped_ext r(*this);
@@ -253,7 +233,7 @@ public:
     struct reg {
         unsigned m_ext_id;
         reg() {
-            register_scoped_ext(get_class_name(), using_namespace_fn, export_namespace_fn, push_fn, pop_fn);
+            register_scoped_ext(get_class_name(), using_namespace_fn, push_fn, pop_fn);
             register_module_object_reader(get_serialization_key(), reader);
             m_ext_id = environment::register_extension(std::make_shared<scoped_ext>());
         }
@@ -272,9 +252,6 @@ public:
     static environment using_namespace_fn(environment const & env, io_state const & ios, name const & n) {
         return update(env, get(env).using_namespace(env, ios, n));
     }
-    static environment export_namespace_fn(environment const & env, io_state const & ios, name const & n) {
-        return get(env).export_namespace(env, ios, n);
-    }
     static environment push_fn(environment const & env, io_state const &, scope_kind) {
         return update(env, get(env).push());
     }