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,