always export Pure theory;

--- a/src/Pure/ROOT	Wed Aug 01 22:59:42 2018 +0100
+++ b/src/Pure/ROOT	Thu Aug 02 14:21:48 2018 +0200
@@ -4,7 +4,7 @@
   description {*
     The Pure logical framework
   *}
-  options [threads = 1]
+  options [threads = 1, export_theory]
   theories
     Pure (global)
     ML_Bootstrap (global)

--- a/src/Pure/Thy/export_theory.scala	Wed Aug 01 22:59:42 2018 +0100
+++ b/src/Pure/Thy/export_theory.scala	Thu Aug 02 14:21:48 2018 +0200
@@ -122,6 +122,20 @@
     if (cache.isDefined) theory.cache(cache.get) else theory
   }
 
+  def read_pure_theory(store: Sessions.Store, cache: Term.Cache = Term.make_cache()): Theory =
+  {
+    val session_name = Thy_Header.PURE
+    val theory_name = Thy_Header.PURE
+
+    using(store.open_database(session_name))(db =>
+    {
+      db.transaction {
+        read_theory(Export.Provider.database(db, session_name, theory_name),
+          session_name, theory_name, cache = Some(cache))
+      }
+    })
+  }
+
 
   /* entities */