# HG changeset patch
# User wenzelm
# Date 1721404693 -7200
# Node ID 1d6e5b7a6906c2bf905df2f51f39c8d415c41b0f
# Parent  505f97165f52c0ceff46c837cdacaa92b99dd974
more conservative cache: retain concurrent value;

diff -r 505f97165f52 -r 1d6e5b7a6906 src/Pure/General/table.ML
--- 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;