more conservative cache: retain concurrent value;

--- a/src/Pure/General/table.ML	Fri Jul 19 16:58:52 2024 +0200
+++ b/src/Pure/General/table.ML	Fri Jul 19 17:58:13 2024 +0200
@@ -606,8 +606,8 @@
             SOME exn => Exn.reraise exn
           | NONE =>
               (case Exn.result f x of
-                Exn.Res y => (Unsynchronized.change cache1 (update (x, y)); y)
-              | Exn.Exn exn => (Unsynchronized.change cache2 (update (x, exn)); Exn.reraise exn))));
+                Exn.Res y => (Unsynchronized.change cache1 (default (x, y)); y)
+              | Exn.Exn exn => (Unsynchronized.change cache2 (default (x, exn)); Exn.reraise exn))));
     fun reset () = (cache2 := empty; cache1 := empty);
     fun total_size () = size (! cache1) + size (! cache2);
   in {apply = apply, reset = reset, size = total_size} end;