# HG changeset patch
# User wenzelm
# Date 1527846620 -7200
# Node ID b44010800a190c9cb27618e150a86bfbb5833cac
# Parent  5bc1e1ac79552ec44b8298f4a41bdf714ee6fe56
tuned signature;

diff -r 5bc1e1ac7955 -r b44010800a19 src/Pure/Thy/export_theory.scala
--- a/src/Pure/Thy/export_theory.scala	Fri Jun 01 11:10:22 2018 +0200
+++ b/src/Pure/Thy/export_theory.scala	Fri Jun 01 11:50:20 2018 +0200
@@ -60,6 +60,8 @@
 
   /** theory content **/
 
+  val export_prefix: String = "theory/"
+
   sealed case class Theory(name: String, parents: List[String],
     types: List[Type],
     consts: List[Const],
@@ -100,7 +102,7 @@
     cache: Option[Term.Cache] = None): Theory =
   {
     val parents =
-      Export.read_entry(db, session_name, theory_name, "theory/parents") match {
+      Export.read_entry(db, session_name, theory_name, export_prefix + "parents") match {
         case Some(entry) => split_lines(entry.uncompressed().text)
         case None =>
           error("Missing theory export in session " + quote(session_name) + ": " +
@@ -147,7 +149,7 @@
   def read_export[A](db: SQL.Database, session_name: String, theory_name: String,
     export_name: String, decode: XML.Body => List[A]): List[A] =
   {
-    Export.read_entry(db, session_name, theory_name, "theory/" + export_name) match {
+    Export.read_entry(db, session_name, theory_name, export_prefix + export_name) match {
       case Some(entry) => decode(entry.uncompressed_yxml())
       case None => Nil
     }