src/Pure/Thy/thy_info.scala

     def errors: List[String] = entries.flatMap(_.header.errors)
 
     lazy val syntax: Outer_Syntax =
       resources.session_base.syntax.add_keywords(keywords).add_abbrevs(abbrevs)
 
-    def loaded_theories: Set[String] =
-      resources.session_base.loaded_theories ++ rev_entries.map(_.name.theory)
+    def loaded_theories: Graph[String, Outer_Syntax] =
+      (resources.session_base.loaded_theories /: entries)({ case (graph, entry) =>
+        val name = entry.name.theory
+        val imports = entry.header.imports.map(p => p._1.theory)
+
+        if (graph.defined(name))
+          error("Duplicate loaded theory entry " + quote(name))
+
+        for (dep <- imports if !graph.defined(dep))
+          error("Missing loaded theory entry " + quote(dep) + " for " + quote(name))
+
+        val syntax = Outer_Syntax.merge(imports.map(graph.get_node(_))) + entry.header
+        (graph.new_node(name, syntax) /: imports)((g, dep) => g.add_edge(dep, name))
+      })
 
     def loaded_files: List[(String, List[Path])] =
     {
       names.map(_.theory) zip
         Par_List.map((e: () => List[Path]) => e(), names.map(resources.loaded_files(syntax, _)))