src/Pure/Thy/sessions.scala

         theories_local = for ((a, b) <- theories_local) yield (a, b.map(File.standard_path(_))),
         files = for ((a, b) <- files) yield (a, b.map(c => c.map(File.standard_path(_)))))
 
     def theory_names: List[Document.Node.Name] = theories.iterator.map(p => p._2.name).toList
 
-    lazy val theory_graph: Document.Theory_Graph[Unit] =
-      Document.theory_graph(
+    lazy val theory_graph: Document.Node.Name.Graph[Unit] =
+      Document.Node.Name.make_graph(
         for ((_, entry) <- theories.toList)
         yield ((entry.name, ()), entry.header.imports.map(imp => theories(imp.theory).name)))
 
     def get_file(file: JFile, bootstrap: Boolean = false): Option[Document.Node.Name] =
     {

       (for {
         (_, base) <- session_bases.iterator
         name <- base.dump_checkpoints.iterator
       } yield name).toSet
 
-    def used_theories_condition(
-      default_options: Options, progress: Progress = No_Progress): Document.Theory_Graph[Options] =
+    def used_theories_condition(default_options: Options, progress: Progress = No_Progress)
+      : Document.Node.Name.Graph[Options] =
     {
       val default_skip_proofs = default_options.bool("skip_proofs")
-      Document.theory_graph(
+      Document.Node.Name.make_graph(
         permissive = true,
         entries =
           for {
             session_name <- sessions_structure.build_topological_order
             entry @ ((name, options), _) <- session_bases(session_name).used_theories