src/Pure/PIDE/resources.scala

       errors match {
         case Nil => this
         case errs => error(cat_lines(errs))
       }
 
-    lazy val theory_graph: Document.Theory_Graph[A] =
-      Document.theory_graph(entries.map(entry =>
-        ((entry.name, seen(entry.name)), entry.header.imports)))
+    lazy val theory_graph: Document.Theory_Graph[Unit] =
+    {
+      val regular = theories.toSet
+      val irregular =
+        (for {
+          entry <- entries.iterator
+          imp <- entry.header.imports
+          if !regular(imp)
+        } yield imp).toSet
+
+      Document.theory_graph(
+        irregular.toList.map(name => ((name, ()), Nil)) :::
+        entries.map(entry => ((entry.name, ()), entry.header.imports)))
+    }
 
     lazy val loaded_theories: Graph[String, Outer_Syntax] =
       (session_base.loaded_theories /: entries)({ case (graph, entry) =>
         val name = entry.name.theory
         val imports = entry.header.imports.map(_.theory)