src/Pure/Thy/sessions.scala

       global_theories: Map[String, String] = Map.empty,
       all_known: Boolean = false): Deps =
   {
     val session_bases =
       (Map.empty[String, Base] /: sessions.imports_topological_order)({
-        case (session_bases, (session_name, info)) =>
+        case (session_bases, info) =>
           if (progress.stopped) throw Exn.Interrupt()
 
           try {
             val parent_base: Sessions.Base =
               info.parent match {

             val imports_base: Sessions.Base =
               parent_base.copy(known =
                 Known.make(info.dir, parent_base :: info.imports.map(session_bases(_)), Nil))
 
             val resources = new Resources(imports_base,
-              default_qualifier = info.theory_qualifier(session_name))
+              default_qualifier = info.theory_qualifier(info.name))
 
             if (verbose || list_files) {
               val groups =
                 if (info.groups.isEmpty) ""
                 else info.groups.mkString(" (", " ", ")")
-              progress.echo("Session " + info.chapter + "/" + session_name + groups)
+              progress.echo("Session " + info.chapter + "/" + info.name + groups)
             }
 
             val thy_deps =
             {
               val root_theories =
                 info.theories.flatMap({ case (_, thys) =>
                   thys.map({ case (thy, pos) =>
-                    (resources.import_name(session_name, info.dir.implode, thy), pos) })
+                    (resources.import_name(info.name, info.dir.implode, thy), pos) })
                 })
               val thy_deps = resources.thy_info.dependencies(root_theories)
 
               thy_deps.errors match {
                 case Nil => thy_deps

 
             val theory_files = thy_deps.deps.map(dep => Path.explode(dep.name.node))
             val loaded_files =
               if (inlined_files) {
                 val pure_files =
-                  if (is_pure(session_name)) {
+                  if (is_pure(info.name)) {
                     val roots = Thy_Header.ml_roots.map(p => info.dir + Path.explode(p._1))
                     val files =
                       roots.flatMap(root => resources.loaded_files(syntax, File.read(root))).
                         map(file => info.dir + Path.explode(file))
                     roots ::: files

                 Graph_Display.Node("[" + name + "]", "session." + name)
 
               def node(name: Document.Node.Name): Graph_Display.Node =
               {
                 val session = resources.theory_qualifier(name)
-                if (session == session_name)
+                if (session == info.name)
                   Graph_Display.Node(name.theory_base_name, "theory." + name.theory)
                 else session_node(session)
               }
 
               val imports_subgraph =

                 keywords = thy_deps.keywords,
                 syntax = syntax,
                 sources = all_files.map(p => (p, SHA1.digest(p.file))),
                 session_graph = session_graph)
 
-            session_bases + (session_name -> base)
+            session_bases + (info.name -> base)
           }
           catch {
             case ERROR(msg) =>
               cat_error(msg, "The error(s) above occurred in session " +
-                quote(session_name) + Position.here(info.pos))
+                quote(info.name) + Position.here(info.pos))
           }
       })
 
     Deps(session_bases,
       if (all_known) Known.make(Path.current, session_bases.toList.map(_._2), Nil)

 
 
   /* cumulative session info */
 
   sealed case class Info(
+    name: String,
     chapter: String,
     select: Boolean,
     pos: Position.T,
     groups: List[String],
     dir: Path,

       if (imports_graph.defined(name)) Some(imports_graph.get_node(name)) else None
 
     def global_theories: Map[String, String] =
       (Thy_Header.bootstrap_global_theories.toMap /:
         (for {
-          (session_name, (info, _)) <- imports_graph.iterator
-          thy <- info.global_theories.iterator } yield (thy, session_name, info)))({
-            case (global, (thy, session_name, info)) =>
-              val qualifier = info.theory_qualifier(session_name)
+          (_, (info, _)) <- imports_graph.iterator
+          thy <- info.global_theories.iterator }
+         yield (thy, info)))({
+            case (global, (thy, info)) =>
+              val qualifier = info.theory_qualifier(info.name)
               global.get(thy) match {
                 case Some(qualifier1) if qualifier != qualifier1 =>
                   error("Duplicate global theory " + quote(thy) + Position.here(info.pos))
                 case _ => global + (thy -> qualifier)
               }

       build_graph.all_preds(List(name)).tail.reverse
 
     def build_descendants(names: List[String]): List[String] =
       build_graph.all_succs(names)
 
-    def build_topological_order: List[(String, Info)] =
-      build_graph.topological_order.map(name => (name, apply(name)))
-
-    def imports_topological_order: List[(String, Info)] =
-      imports_graph.topological_order.map(name => (name, apply(name)))
+    def build_topological_order: List[Info] =
+      build_graph.topological_order.map(apply(_))
+
+    def imports_topological_order: List[Info] =
+      imports_graph.topological_order.map(apply(_))
 
     override def toString: String =
       imports_graph.keys_iterator.mkString("Sessions.T(", ", ", ")")
   }
 

           val meta_digest =
             SHA1.digest((entry_chapter, name, entry.parent, entry.options,
               entry.imports, entry.theories, entry.files, entry.document_files).toString)
 
           val info =
-            Info(entry_chapter, select, entry.pos, entry.groups, dir + Path.explode(entry.path),
-              entry.parent, entry.description, session_options, entry.imports, theories,
-              global_theories, files, document_files, meta_digest)
+            Info(name, entry_chapter, select, entry.pos, entry.groups,
+              dir + Path.explode(entry.path), entry.parent, entry.description, session_options,
+              entry.imports, theories, global_theories, files, document_files, meta_digest)
 
           (name, info)
         }
         catch {
           case ERROR(msg) =>