diff --git a/src/library/export_decl.cpp b/src/library/export_decl.cpp
index de14d5b403..9c21596f04 100644
--- a/src/library/export_decl.cpp
+++ b/src/library/export_decl.cpp
@@ -64,6 +64,18 @@ static environment update(environment const & env, export_decl_env_ext const & e
     return env.update(g_ext->m_ext_id, std::make_shared<export_decl_env_ext>(ext));
 }
 
+static environment add_export_decl_core(environment const & env, name const & in_ns, export_decl const & e) {
+    auto ns_map = get_export_decl_extension(env).m_ns_map;
+    list<export_decl> decls;
+    if (ns_map.contains(in_ns))
+        decls = *ns_map.find(in_ns);
+
+    if (std::find(decls.begin(), decls.end(), e) != decls.end())
+        return env;
+
+    return update(env, export_decl_env_ext(insert(ns_map, in_ns, cons(e, decls))));
+}
+
 struct export_decl_modification : public modification {
     LEAN_MODIFICATION("export_decl")
 
@@ -75,7 +87,7 @@ struct export_decl_modification : public modification {
         m_in_ns(in_ns), m_export_decl(e) {}
 
     void perform(environment & env) const override {
-        env = add_export_decl(env, m_in_ns, m_export_decl);
+        env = add_export_decl_core(env, m_in_ns, m_export_decl);
     }
 
     void serialize(serializer & s) const override {
@@ -95,17 +107,10 @@ struct export_decl_modification : public modification {
 };
 
 environment add_export_decl(environment const & env, name const & in_ns, export_decl const & e) {
-    auto ns_map = get_export_decl_extension(env).m_ns_map;
-    list<export_decl> decls;
-    if (ns_map.contains(in_ns))
-        decls = *ns_map.find(in_ns);
-
-    if (std::find(decls.begin(), decls.end(), e) != decls.end())
-        return env;
-
-    auto new_env = update(env, export_decl_env_ext(insert(ns_map, in_ns, cons(e, decls))));
+    environment new_env = add_export_decl_core(env, in_ns, e);
     return module::add(new_env, std::make_shared<export_decl_modification>(in_ns, e));
 }
+
 environment add_export_decl(environment const & env, export_decl const & entry) {
     return add_export_decl(env, get_namespace(env), entry);
 }