diff -r cc711d229815 -r 642ecd97d35c src/Pure/Thy/export_theory.scala
--- 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,