src/Pure/Thy/sessions.scala

             }
 
             val thy_deps =
             {
               val root_theories =
-                info.theories.flatMap({
-                  case (_, _, thys) =>
-                    thys.map(thy =>
-                      (resources.init_name(info.dir + resources.thy_path(thy)), info.pos))
+                info.theories.flatMap({ case (_, thys) =>
+                  thys.map(thy =>
+                    (resources.init_name(info.dir + resources.thy_path(thy)), info.pos))
                 })
               val thy_deps = resources.thy_info.dependencies(root_theories)
 
               thy_deps.errors match {
                 case Nil => thy_deps

     groups: List[String],
     dir: Path,
     parent: Option[String],
     description: String,
     options: Options,
-    theories: List[(Boolean, Options, List[Path])],
+    theories: List[(Options, List[Path])],
+    global_theories: List[String],
     files: List[Path],
     document_files: List[(Path, Path)],
     meta_digest: SHA1.Digest)
   {
     def timeout: Time = Time.seconds(options.real("timeout") * options.real("timeout_scale"))
-
-    def global_theories: List[String] =
-      for { (global, _, paths) <- theories if global; path <- paths }
-      yield {
-        val name = path.base.implode
-        if (Long_Name.is_qualified(name))
-          error("Bad qualified name for global theory " + quote(name))
-        else name
-      }
   }
 
   object Tree
   {
     def apply(infos: Traversable[(String, Info)]): Tree =

   private val CHAPTER = "chapter"
   private val SESSION = "session"
   private val IN = "in"
   private val DESCRIPTION = "description"
   private val OPTIONS = "options"
-  private val GLOBAL_THEORIES = "global_theories"
   private val THEORIES = "theories"
+  private val GLOBAL = "global"
   private val FILES = "files"
   private val DOCUMENT_FILES = "document_files"
 
   lazy val root_syntax =
-    Outer_Syntax.init() + "(" + ")" + "+" + "," + "=" + "[" + "]" + IN +
+    Outer_Syntax.init() + "(" + ")" + "+" + "," + "=" + "[" + "]" + GLOBAL + IN +
       (CHAPTER, Keyword.THY_DECL) +
       (SESSION, Keyword.THY_DECL) +
       (DESCRIPTION, Keyword.QUASI_COMMAND) +
       (OPTIONS, Keyword.QUASI_COMMAND) +
-      (GLOBAL_THEORIES, Keyword.QUASI_COMMAND) +
       (THEORIES, Keyword.QUASI_COMMAND) +
       (FILES, Keyword.QUASI_COMMAND) +
       (DOCUMENT_FILES, Keyword.QUASI_COMMAND)
 
   private object Parser extends Parse.Parser with Options.Parser

       groups: List[String],
       path: String,
       parent: Option[String],
       description: String,
       options: List[Options.Spec],
-      theories: List[(Boolean, List[Options.Spec], List[String])],
+      theories: List[(List[Options.Spec], List[(String, Boolean)])],
       files: List[String],
       document_files: List[(String, String)]) extends Entry
 
     private val chapter: Parser[Chapter] =
     {

       val option =
         option_name ~ opt($$$("=") ~! option_value ^^
           { case _ ~ x => x }) ^^ { case x ~ y => (x, y) }
       val options = $$$("[") ~> rep1sep(option, $$$(",")) <~ $$$("]")
 
+      val global =
+        ($$$("(") ~! $$$(GLOBAL) ~ $$$(")")) ^^ { case _ => true } | success(false)
+
+      val theory_entry =
+        theory_name ~ global ^^ { case x ~ y => (x, y) }
+
       val theories =
-        ($$$(GLOBAL_THEORIES) | $$$(THEORIES)) ~!
-          ((options | success(Nil)) ~ rep(theory_name)) ^^
-          { case x ~ (y ~ z) => (x == GLOBAL_THEORIES, y, z) }
+        $$$(THEORIES) ~!
+          ((options | success(Nil)) ~ rep(theory_entry)) ^^
+          { case _ ~ (x ~ y) => (x, y) }
 
       val document_files =
         $$$(DOCUMENT_FILES) ~!
           (($$$("(") ~! ($$$(IN) ~! (path ~ $$$(")"))) ^^
               { case _ ~ (_ ~ (x ~ _)) => x } | success("document")) ~

           if (!is_pure(name) && !entry.parent.isDefined) error("Missing parent session")
 
           val session_options = options ++ entry.options
 
           val theories =
-            entry.theories.map({ case (global, opts, thys) =>
-              (global, session_options ++ opts, thys.map(Path.explode(_))) })
+            entry.theories.map({ case (opts, thys) =>
+              (session_options ++ opts, thys.map(thy => Path.explode(thy._1))) })
+
+          val global_theories =
+            for { (_, thys) <- entry.theories; (thy, global) <- thys if global }
+            yield {
+              val thy_name = Path.explode(thy).expand.base.implode
+              if (Long_Name.is_qualified(thy_name))
+                error("Bad qualified name for global theory " + quote(thy_name))
+              else thy_name
+            }
+
           val files = entry.files.map(Path.explode(_))
           val document_files =
             entry.document_files.map({ case (s1, s2) => (Path.explode(s1), Path.explode(s2)) })
 
           val meta_digest =
             SHA1.digest((entry_chapter, name, entry.parent, entry.options,
               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, theories, files,
-              document_files, meta_digest)
+              entry.parent, entry.description, session_options, theories, global_theories,
+              files, document_files, meta_digest)
 
           (name, info)
         }
         catch {
           case ERROR(msg) =>