--- a/src/Pure/Thy/export_theory.scala Sat Jul 30 11:10:39 2022 +0200
+++ b/src/Pure/Thy/export_theory.scala Sat Jul 30 11:35:04 2022 +0200
@@ -80,7 +80,7 @@
) {
override def toString: String = name
- def entity_iterator: Iterator[Entity[No_Content]] =
+ def entity_iterator: Iterator[Entity0] =
types.iterator.map(_.no_content) ++
consts.iterator.map(_.no_content) ++
axioms.iterator.map(_.no_content) ++
@@ -213,7 +213,7 @@
def the_content: A =
if (content.isDefined) content.get else error("No content for " + toString)
- def no_content: Entity[No_Content] = copy(content = None)
+ def no_content: Entity0 = copy(content = None)
def cache(cache: Term.Cache): Entity[A] =
Entity(
@@ -225,6 +225,7 @@
serial,
content.map(_.cache(cache)))
}
+ type Entity0 = Entity[No_Content]
def read_entities[A <: Content[A]](
provider: Export.Provider,