clarified signature;

--- a/src/Pure/General/xz.scala	Fri Jun 19 16:12:32 2020 +0200
+++ b/src/Pure/General/xz.scala	Fri Jun 19 18:22:03 2020 +0200
@@ -28,6 +28,7 @@
 
   type Cache = ArrayCache
 
+  def no_cache(): ArrayCache = ArrayCache.getDummyCache()
   def cache(): ArrayCache = ArrayCache.getDefaultCache()
   def make_cache(): ArrayCache = new BasicArrayCache
 }