# HG changeset patch
# User wenzelm
# Date 1526823436 -7200
# Node ID 0004e7a9fa10d27c2013496550e1ad3a2260bec0
# Parent  9bee37c2ac2b2e32df287e32fe4cee13156768f3
clarified encoding;

diff -r 9bee37c2ac2b -r 0004e7a9fa10 src/Pure/Thy/export_theory.ML
--- a/src/Pure/Thy/export_theory.ML	Sun May 20 15:28:59 2018 +0200
+++ b/src/Pure/Thy/export_theory.ML	Sun May 20 15:37:16 2018 +0200
@@ -32,8 +32,7 @@
     val parents = Theory.parents_of thy;
     val _ =
       export_body thy "parents"
-        let open XML.Encode
-        in list string (map Context.theory_long_name parents) end;
+        (XML.Encode.string (cat_lines (map Context.theory_long_name parents)));
 
 
     (* entities *)
diff -r 9bee37c2ac2b -r 0004e7a9fa10 src/Pure/Thy/export_theory.scala
--- a/src/Pure/Thy/export_theory.scala	Sun May 20 15:28:59 2018 +0200
+++ b/src/Pure/Thy/export_theory.scala	Sun May 20 15:37:16 2018 +0200
@@ -68,9 +68,7 @@
   {
     val parents =
       Export.read_entry(db, session_name, theory_name, "theory/parents") match {
-        case Some(entry) =>
-          import XML.Decode._
-          list(string)(entry.uncompressed_yxml())
+        case Some(entry) => split_lines(entry.uncompressed().text)
         case None =>
           error("Missing theory export in session " + quote(session_name) + ": " +
             quote(theory_name))