# HG changeset patch
# User wenzelm
# Date 1533239371 -7200
# Node ID d1d03b7b6696b0e5f68cda10e723dc2379826e82
# Parent  3db37e950118b9d9acbc7c68fbc42a51b96e62ef
tuned signature;

diff -r 3db37e950118 -r d1d03b7b6696 src/Pure/Thy/export_theory.scala
--- a/src/Pure/Thy/export_theory.scala	Thu Aug 02 14:21:48 2018 +0200
+++ b/src/Pure/Thy/export_theory.scala	Thu Aug 02 21:49:31 2018 +0200
@@ -75,6 +75,14 @@
   {
     override def toString: String = name
 
+    lazy val entities: Set[Long] =
+      Set.empty[Long] ++
+        types.iterator.map(_.entity.serial) ++
+        consts.iterator.map(_.entity.serial) ++
+        axioms.iterator.map(_.entity.serial) ++
+        facts.iterator.map(_.entity.serial) ++
+        classes.iterator.map(_.entity.serial)
+
     def cache(cache: Term.Cache): Theory =
       Theory(cache.string(name),
         parents.map(cache.string(_)),
@@ -122,7 +130,7 @@
     if (cache.isDefined) theory.cache(cache.get) else theory
   }
 
-  def read_pure_theory(store: Sessions.Store, cache: Term.Cache = Term.make_cache()): Theory =
+  def read_pure_theory(store: Sessions.Store, cache: Option[Term.Cache] = None): Theory =
   {
     val session_name = Thy_Header.PURE
     val theory_name = Thy_Header.PURE
@@ -131,7 +139,7 @@
     {
       db.transaction {
         read_theory(Export.Provider.database(db, session_name, theory_name),
-          session_name, theory_name, cache = Some(cache))
+          session_name, theory_name, cache = cache)
       }
     })
   }