tuned;

--- a/src/Pure/General/cache.scala	Wed Jan 15 19:46:04 2020 +0100
+++ b/src/Pure/General/cache.scala	Wed Jan 15 19:49:13 2020 +0100
@@ -24,11 +24,7 @@
   {
     val ref = table.get(x)
     if (ref == null) None
-    else {
-      val y = ref.asInstanceOf[WeakReference[A]].get
-      if (y == null) None
-      else Some(y)
-    }
+    else Option(ref.asInstanceOf[WeakReference[A]].get)
   }
 
   protected def store[A](x: A): A =