diff -r a23e0964f3c3 -r 9dda93a753b1 src/Pure/Thy/export_theory.scala
--- a/src/Pure/Thy/export_theory.scala	Mon Dec 07 19:45:52 2020 +0100
+++ b/src/Pure/Thy/export_theory.scala	Mon Dec 07 20:26:09 2020 +0100
@@ -41,7 +41,7 @@
             for (theory <- Export.read_theory_names(db, session))
             yield {
               progress.echo("Reading theory " + theory)
-              read_theory(Export.Provider.database(db, session, theory),
+              read_theory(Export.Provider.database(db, store.xz_cache, session, theory),
                 session, theory, cache = Some(cache))
             }
           }
@@ -113,7 +113,7 @@
       if (theory_name == Thy_Header.PURE) Nil
       else {
         provider(Export.THEORY_PREFIX + "parents") match {
-          case Some(entry) => split_lines(entry.uncompressed().text)
+          case Some(entry) => split_lines(entry.uncompressed.text)
           case None =>
             error("Missing theory export in session " + quote(session_name) + ": " +
               quote(theory_name))
@@ -145,7 +145,8 @@
     using(store.open_database(session_name))(db =>
     {
       db.transaction {
-        read(Export.Provider.database(db, session_name, theory_name), session_name, theory_name)
+        read(Export.Provider.database(
+          db, store.xz_cache, session_name, theory_name), session_name, theory_name)
       }
     })
   }
@@ -378,7 +379,7 @@
   {
     for { entry <- provider.focus(id.theory_name)(Export.PROOFS_PREFIX + id.serial) }
     yield {
-      val body = entry.uncompressed_yxml()
+      val body = entry.uncompressed_yxml
       val (typargs, (args, (prop_body, proof_body))) =
       {
         import XML.Decode._