src/Pure/General/table.ML

--- a/src/Pure/General/table.ML	Mon Dec 02 18:53:45 2024 +0100
+++ b/src/Pure/General/table.ML	Mon Dec 02 20:35:12 2024 +0100
@@ -68,6 +68,7 @@
   val make_set: key list -> set
   type 'a cache_ops = {apply: key -> 'a, reset: unit -> unit, size: unit -> int}
   val unsynchronized_cache: (key -> 'a) -> 'a cache_ops
+  val apply_unsynchronized_cache: (key -> 'a) -> key -> 'a
 end;
 
 functor Table(Key: KEY): TABLE =
@@ -610,6 +611,8 @@
     fun total_size () = size (! cache1) + size (! cache2);
   in {apply = apply, reset = reset, size = total_size} end;
 
+fun apply_unsynchronized_cache f = #apply (unsynchronized_cache f);
+
 
 (* ML pretty-printing *)