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(""".*?([^/\\:]+)""")