diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp
index 088e3de5e7..7b7f2ba3ab 100644
--- a/src/frontends/lean/builtin_cmds.cpp
+++ b/src/frontends/lean/builtin_cmds.cpp
@@ -61,7 +61,7 @@ environment section_cmd(parser & p) {
 // Execute open command
 environment execute_open(environment env, io_state const & ios, export_decl const & edecl);
 
-environment replay_export_decls(environment env, io_state const & ios, unsigned old_sz) {
+environment replay_export_decls_core(environment env, io_state const & ios, unsigned old_sz) {
     list<export_decl> new_export_decls = get_export_decls(env);
     unsigned new_sz = length(new_export_decls);
     lean_assert(new_sz >= old_sz);
@@ -75,6 +75,10 @@ environment replay_export_decls(environment env, io_state const & ios, unsigned
     return env;
 }
 
+environment replay_export_decls_core(environment env, io_state const & ios) {
+    return replay_export_decls_core(env, ios, 0);
+}
+
 environment execute_open(environment env, io_state const & ios, export_decl const & edecl) {
     unsigned fingerprint = 0;
     for (name const & n : edecl.m_metacls)
@@ -102,7 +106,7 @@ environment execute_open(environment env, io_state const & ios, export_decl cons
         }
     }
     env = update_fingerprint(env, fingerprint);
-    return replay_export_decls(env, ios, old_export_decls_sz);
+    return replay_export_decls_core(env, ios, old_export_decls_sz);
 }
 
 environment namespace_cmd(parser & p) {
@@ -110,7 +114,7 @@ environment namespace_cmd(parser & p) {
     p.push_local_scope();
     unsigned old_export_decls_sz = length(get_export_decls(p.env()));
     environment env = push_scope(p.env(), p.ios(), scope_kind::Namespace, n);
-    return replay_export_decls(env, p.ios(), old_export_decls_sz);
+    return replay_export_decls_core(env, p.ios(), old_export_decls_sz);
 }
 
 static environment redeclare_aliases(environment env, parser & p,
diff --git a/src/frontends/lean/builtin_cmds.h b/src/frontends/lean/builtin_cmds.h
index cfe20faed9..1d7135c451 100644
--- a/src/frontends/lean/builtin_cmds.h
+++ b/src/frontends/lean/builtin_cmds.h
@@ -11,6 +11,9 @@ bool print_id_info(parser & p, name const & id, bool show_value, pos_info const
 bool print_token_info(parser const & p, name const & tk);
 
 cmd_table get_builtin_cmds();
+/* \brief Replay export declarations in the top-level of imported files */
+environment replay_export_decls_core(environment env, io_state const & ios);
+
 void initialize_builtin_cmds();
 void finalize_builtin_cmds();
 }
diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index a74c7c649c..18380ea0c4 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -1907,6 +1907,7 @@ void parser::parse_imports() {
     m_env = import_modules(m_env, base, olean_files.size(), olean_files.data(), num_threads,
                            keep_imported_thms, m_ios);
     m_env = update_fingerprint(m_env, fingerprint);
+    m_env = replay_export_decls_core(m_env, m_ios);
     if (imported)
         commit_info(1, 0);
 }