src/Pure/Thy/export.scala
changeset 73024 337e1b135d2f
parent 72854 6c660f05f70c
child 73031 f93f0597f4fb
--- a/src/Pure/Thy/export.scala	Sat Jan 02 14:24:03 2021 +0100
+++ b/src/Pure/Thy/export.scala	Sat Jan 02 15:58:48 2021 +0100
@@ -85,7 +85,7 @@
   def compound_name(a: String, b: String): String = a + ":" + b
 
   def empty_entry(theory_name: String, name: String): Entry =
-    Entry("", theory_name, name, false, Future.value(false, Bytes.empty), XZ.no_cache())
+    Entry("", theory_name, name, false, Future.value(false, Bytes.empty), XZ.Cache.none)
 
   sealed case class Entry(
     session_name: String,