src/Pure/Thy/export_theory.scala
changeset 68231 0004e7a9fa10
parent 68222 3c1a716e7f59
child 68232 4b93573ac5b4
--- 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))