# HG changeset patch
# User wenzelm
# Date 1579114153 -3600
# Node ID 6316debd3a9f422f3a32f3f43ceecdd9bda90b30
# Parent  b9ea2467c929c48b189b0103e9c3cb3a67f708f8
tuned;

diff -r b9ea2467c929 -r 6316debd3a9f src/Pure/General/cache.scala
--- 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 =