diff --git a/src/library/module.cpp b/src/library/module.cpp
index 42f31c502a..dfaf0c3091 100644
--- a/src/library/module.cpp
+++ b/src/library/module.cpp
@@ -300,6 +300,11 @@ struct decl_modification : public modification {
     static std::shared_ptr<modification const> deserialize(deserializer & d) {
         return std::make_shared<decl_modification>(read_declaration(d));
     }
+
+    void get_task_dependencies(std::vector<generic_task_result> & deps) const override {
+        if (m_decl.is_theorem())
+            deps.push_back(m_decl.get_value_task());
+    }
 };
 
 struct inductive_modification : public modification {
diff --git a/src/library/module.h b/src/library/module.h
index 3115088d2a..922f5917f3 100644
--- a/src/library/module.h
+++ b/src/library/module.h
@@ -91,6 +91,7 @@ public:
     virtual const char * get_key() const = 0;
     virtual void perform(environment &) const = 0;
     virtual void serialize(serializer &) const = 0;
+    virtual void get_task_dependencies(std::vector<generic_task_result> &) const {}
 };
 
 #define LEAN_MODIFICATION(k) \
diff --git a/src/library/module_mgr.cpp b/src/library/module_mgr.cpp
index 57228fd1fc..ca7de06d0d 100644
--- a/src/library/module_mgr.cpp
+++ b/src/library/module_mgr.cpp
@@ -112,9 +112,8 @@ public:
     std::vector<generic_task_result> get_dependencies() override {
         if (auto res = m_mod->m_result.peek()) {
             std::vector<generic_task_result> deps;
-            res->m_env->for_each_declaration([&] (declaration const & d) {
-                if (d.is_theorem()) deps.push_back(d.get_value_task());
-            });
+            for (auto & mdf : res->m_loaded_module->m_modifications)
+                mdf->get_task_dependencies(deps);
             return deps;
         } else {
             return {m_mod->m_result};