src/Pure/Thy/export.scala

--- a/src/Pure/Thy/export.scala	Fri Aug 12 15:57:22 2022 +0200
+++ b/src/Pure/Thy/export.scala	Fri Aug 12 16:01:52 2022 +0200
@@ -420,7 +420,7 @@
         entry_name <- entry_names(session = session).iterator
         if matcher(entry_name)
         entry <- get(entry_name.theory, entry_name.name).iterator
-      } yield File.Content(entry.entry_name.make_path(), entry.uncompressed)).toList
+      } yield File.content(entry.entry_name.make_path(), entry.uncompressed)).toList
   }
 
   override def toString: String =