# HG changeset patch
# User wenzelm
# Date 1533212508 -7200
# Node ID 3db37e950118b9d9acbc7c68fbc42a51b96e62ef
# Parent  6d9eca4805ff91f6ee3f0e8dbdd1ce10eca83d02
always export Pure theory;

diff -r 6d9eca4805ff -r 3db37e950118 src/Pure/ROOT
--- 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)
diff -r 6d9eca4805ff -r 3db37e950118 src/Pure/Thy/export_theory.scala
--- 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 */