--- 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))