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 */