# HG changeset patch
# User wenzelm
# Date 1672497953 -3600
# Node ID e37c58cbb79fadaa0153263608b851dc7038a22d
# Parent  2915740fce1f619cebba9e733159a61fb379c91f
tuned;

diff -r 2915740fce1f -r e37c58cbb79f src/Pure/Thy/export_theory.scala
--- a/src/Pure/Thy/export_theory.scala	Sat Dec 31 15:42:13 2022 +0100
+++ b/src/Pure/Thy/export_theory.scala	Sat Dec 31 15:45:53 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.bytes.text))
+      .map(entry => Library.trim_split_lines(entry.text))
 
   def theory_names(
     session_context: Export.Session_Context,
@@ -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.bytes.text)
+        case Some(entry) => split_lines(entry.text)
         case None => Nil
       }
     val other = Other()