diff --git a/src/library/module.cpp b/src/library/module.cpp
index 729b85593..e4c6be9e0 100644
--- a/src/library/module.cpp
+++ b/src/library/module.cpp
@@ -129,8 +129,13 @@ static register_module_object_reader_fn g_reg_decl_reader(g_decl, declaration_re
 
 environment add(environment const & env, certified_declaration const & d) {
     environment new_env = env.add(d);
-    new_env = add(new_env, g_decl, [=](serializer & s) { s << d.get_declaration(); });
-    return new_env;
+    declaration _d = d.get_declaration();
+    return add(new_env, g_decl, [=](serializer & s) { s << _d; });
+}
+
+environment add(environment const & env, declaration const & d) {
+    environment new_env = env.add(d);
+    return add(new_env, g_decl, [=](serializer & s) { s << d; });
 }
 
 struct import_modules_fn {
diff --git a/src/library/module.h b/src/library/module.h
index f61d8b29a..0ee5ae25a 100644
--- a/src/library/module.h
+++ b/src/library/module.h
@@ -70,4 +70,9 @@ environment add(environment const & env, std::string const & k, std::function<vo
 
 /** \brief Add the given declaration to the environment, and mark it to be exported. */
 environment add(environment const & env, certified_declaration const & d);
+/**
+    \brief Add the given declaration to the environment, and mark it to be exported.
+    This method throws an exception if the trust_level <= LEAN_BELIEVER_TRUST_LEVEL
+*/
+environment add(environment const & env, declaration const & d);
 }