author | wenzelm |
Wed, 04 Aug 2021 21:49:17 +0200 | |
changeset 74120 | 21ddf56ac140 |
parent 74118 | 49884e54f13a (current diff) |
parent 74119 | 342d0298e164 (diff) |
child 74121 | bc03b0b82fe6 |
--- 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),