diff --git a/src/kernel/declaration.cpp b/src/kernel/declaration.cpp
index 19af64aac..47197cd18 100644
--- a/src/kernel/declaration.cpp
+++ b/src/kernel/declaration.cpp
@@ -81,8 +81,8 @@ declaration mk_definition(environment const & env, name const & n, level_param_n
         });
     return mk_definition(n, params, t, v, opaque, w+1, mod_idx, use_conv_opt);
 }
-declaration mk_theorem(name const & n, level_param_names const & params, expr const & t, expr const & v) {
-    return declaration(new declaration::cell(n, params, t, true, v, true, 0, 0, false));
+declaration mk_theorem(name const & n, level_param_names const & params, expr const & t, expr const & v, module_idx mod_idx) {
+    return declaration(new declaration::cell(n, params, t, true, v, true, 0, mod_idx, false));
 }
 declaration mk_axiom(name const & n, level_param_names const & params, expr const & t) {
     return declaration(new declaration::cell(n, params, t, true));
diff --git a/src/kernel/declaration.h b/src/kernel/declaration.h
index 8feff1e15..62bb30b19 100644
--- a/src/kernel/declaration.h
+++ b/src/kernel/declaration.h
@@ -71,7 +71,7 @@ public:
                                     expr const & v, bool opaque, module_idx mod_idx, bool use_conv_opt);
     friend declaration mk_definition(name const & n, level_param_names const & params, expr const & t, expr const & v, bool opaque,
                                     unsigned weight, module_idx mod_idx, bool use_conv_opt);
-    friend declaration mk_theorem(name const & n, level_param_names const & params, expr const & t, expr const & v);
+    friend declaration mk_theorem(name const & n, level_param_names const & params, expr const & t, expr const & v, module_idx mod_idx);
     friend declaration mk_axiom(name const & n, level_param_names const & params, expr const & t);
     friend declaration mk_var_decl(name const & n, level_param_names const & params, expr const & t);
 };
@@ -84,7 +84,7 @@ declaration mk_definition(name const & n, level_param_names const & params, expr
                          bool opaque = false, unsigned weight = 0, module_idx mod_idx = 0, bool use_conv_opt = true);
 declaration mk_definition(environment const & env, name const & n, level_param_names const & params, expr const & t, expr const & v,
                          bool opaque = false, module_idx mod_idx = 0, bool use_conv_opt = true);
-declaration mk_theorem(name const & n, level_param_names const & params, expr const & t, expr const & v);
+declaration mk_theorem(name const & n, level_param_names const & params, expr const & t, expr const & v, module_idx mod_idx = 0);
 declaration mk_axiom(name const & n, level_param_names const & params, expr const & t);
 declaration mk_var_decl(name const & n, level_param_names const & params, expr const & t);
 }
diff --git a/src/library/kernel_serializer.cpp b/src/library/kernel_serializer.cpp
index 4fa9ee405..ed024ffd9 100644
--- a/src/library/kernel_serializer.cpp
+++ b/src/library/kernel_serializer.cpp
@@ -277,7 +277,7 @@ serializer & operator<<(serializer & s, declaration const & d) {
     return s;
 }
 
-declaration read_declaration(deserializer & d, unsigned module_idx) {
+declaration read_declaration(deserializer & d, module_idx midx) {
     char k               = d.read_char();
     bool has_value       = (k & 1) != 0;
     bool is_th_ax        = (k & 8) != 0;
@@ -287,12 +287,12 @@ declaration read_declaration(deserializer & d, unsigned module_idx) {
     if (has_value) {
         expr v      = read_expr(d);
         if (is_th_ax) {
-            return mk_theorem(n, ps, t, v);
+            return mk_theorem(n, ps, t, v, midx);
         } else {
             unsigned w        = d.read_unsigned();
             bool is_opaque    = (k & 2) != 0;
             bool use_conv_opt = (k & 4) != 0;
-            return mk_definition(n, ps, t, v, is_opaque, w, module_idx, use_conv_opt);
+            return mk_definition(n, ps, t, v, is_opaque, w, midx, use_conv_opt);
         }
     } else {
         if (is_th_ax)
diff --git a/src/library/kernel_serializer.h b/src/library/kernel_serializer.h
index cfa06f8f6..4ce48eee0 100644
--- a/src/library/kernel_serializer.h
+++ b/src/library/kernel_serializer.h
@@ -28,7 +28,7 @@ struct register_macro_deserializer_fn {
 };
 
 serializer & operator<<(serializer & s, declaration const & d);
-declaration read_declaration(deserializer & d, unsigned module_idx);
+declaration read_declaration(deserializer & d, module_idx midx);
 
 typedef std::tuple<level_param_names, unsigned, list<inductive::inductive_decl>> inductive_decls;
 serializer & operator<<(serializer & s, inductive_decls const & ds);
diff --git a/src/library/module.cpp b/src/library/module.cpp
index 63842df68..0211c54e5 100644
--- a/src/library/module.cpp
+++ b/src/library/module.cpp
@@ -265,6 +265,7 @@ struct import_modules_fn {
 
     void import_decl(deserializer & d, module_idx midx) {
         declaration decl = read_declaration(d, midx);
+        lean_assert(!decl.is_definition() || decl.get_module_idx() == midx);
         environment env  = m_senv.env();
         if (env.trust_lvl() > LEAN_BELIEVER_TRUST_LEVEL) {
             if (!m_keep_proofs && decl.is_theorem())