# HG changeset patch
# User wenzelm
# Date 1628106557 -7200
# Node ID 21ddf56ac1409fc59196c799fa60fd85573b7de6
# Parent  49884e54f13af00e280b0108ceb1d97d10765f47# Parent  342d0298e164a8b0f21ac7365b53f36832006f6c
merged

diff -r 49884e54f13a -r 21ddf56ac140 src/Pure/Thy/export_theory.scala
--- a/src/Pure/Thy/export_theory.scala	Wed Aug 04 21:48:50 2021 +0200
+++ b/src/Pure/Thy/export_theory.scala	Wed Aug 04 21:49:17 2021 +0200
@@ -92,6 +92,9 @@
       locales.iterator.map(_.no_content) ++
       locale_dependencies.iterator.map(_.no_content)
 
+    lazy val entity_serials: Set[Long] =
+      entity_iterator.map(_.serial).toSet
+
     def cache(cache: Term.Cache): Theory =
       Theory(cache.string(name),
         parents.map(cache.string),