src/Pure/PIDE/resources.scala

     lazy val overall_syntax: Outer_Syntax =
       Outer_Syntax.merge(loaded_theories.maximals.map(loaded_theories.get_node))
 
     override def toString: String = entries.toString
   }
+
+
+  /* resolve implicit theory dependencies */
+
+  def resolve_dependencies[A](
+    models: Map[A, Document.Model],
+    theories: List[(Document.Node.Name, Position.T)]
+  ): List[Document.Node.Name] = {
+    val model_theories =
+      (for (model <- models.valuesIterator if model.is_theory)
+        yield (model.node_name, Position.none)).toList
+
+    val thy_files1 = dependencies(model_theories ::: theories).theories
+
+    val thy_files2 =
+      (for {
+        model <- models.valuesIterator if !model.is_theory
+        thy_name <- make_theory_name(model.node_name)
+      } yield thy_name).toList
+
+    thy_files1 ::: thy_files2
+  }
 }