# HG changeset patch
# User wenzelm
# Date 1492427641 -7200
# Node ID 571a3ce3cc17fbd1e8a357c1cd024fc6a55fa0e9
# Parent  f3076367f4a861b67eff89c2e97f891a718b4ba2
special theories are always global;

diff -r f3076367f4a8 -r 571a3ce3cc17 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Mon Apr 17 12:29:50 2017 +0200
+++ b/src/Pure/Thy/sessions.scala	Mon Apr 17 13:14:01 2017 +0200
@@ -387,7 +387,7 @@
       if (imports_graph.defined(name)) Some(imports_graph.get_node(name)) else None
 
     def global_theories: Map[String, String] =
-      (Map.empty[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)))({
diff -r f3076367f4a8 -r 571a3ce3cc17 src/Pure/Thy/thy_header.scala
--- a/src/Pure/Thy/thy_header.scala	Mon Apr 17 12:29:50 2017 +0200
+++ b/src/Pure/Thy/thy_header.scala	Mon Apr 17 13:14:01 2017 +0200
@@ -73,10 +73,11 @@
 
   val PURE = "Pure"
   val ML_BOOTSTRAP = "ML_Bootstrap"
-  val ML_ROOT = "ML_Root"
-  val ml_roots = List("ROOT0.ML" -> "ML_Root0", "ROOT.ML" -> ML_ROOT)
+  val ml_roots = List("ROOT0.ML" -> "ML_Root0", "ROOT.ML" -> "ML_Root")
   val bootstrap_thys = List(PURE, ML_BOOTSTRAP).map(a => a -> ("Bootstrap_" + a))
 
+  val bootstrap_global_theories = (ml_roots ::: bootstrap_thys).map(p => (p._2 -> PURE))
+
   private val Thy_File_Name = new Regex(""".*?([^/\\:]+)\.thy""")
   private val Import_Name = new Regex(""".*?([^/\\:]+)""")