--- a/src/Pure/Thy/export_theory.scala Sat Dec 31 15:32:12 2022 +0100
+++ b/src/Pure/Thy/export_theory.scala Sat Dec 31 15:42:13 2022 +0100
@@ -103,7 +103,7 @@
def read_theory_parents(theory_context: Export.Theory_Context): Option[List[String]] =
theory_context.get(Export.THEORY_PREFIX + "parents")
- .map(entry => Library.trim_split_lines(entry.uncompressed.text))
+ .map(entry => Library.trim_split_lines(entry.bytes.text))
def theory_names(
session_context: Export.Session_Context,
@@ -393,7 +393,7 @@
for { entry <- theory_context.get(Export.PROOFS_PREFIX + id.serial) }
yield {
- val body = entry.uncompressed_yxml
+ val body = entry.yxml
val (typargs, (args, (prop_body, proof_body))) = {
import XML.Decode._
import Term_XML.Decode._
@@ -753,7 +753,7 @@
def read_others(theory_context: Export.Theory_Context): Map[String, List[Entity[Other]]] = {
val kinds =
theory_context.get(Export.THEORY_PREFIX + "other_kinds") match {
- case Some(entry) => split_lines(entry.uncompressed.text)
+ case Some(entry) => split_lines(entry.bytes.text)
case None => Nil
}
val other = Other()