--- a/src/Pure/term_items.ML Fri Dec 08 13:09:39 2023 +0100
+++ b/src/Pure/term_items.ML Fri Dec 08 13:36:47 2023 +0100
@@ -33,6 +33,7 @@
val make2: key * 'a -> key * 'a -> 'a table
val make3: key * 'a -> key * 'a -> key * 'a -> 'a table
val make_strict: (key * 'a) list -> 'a table
+ val unsynchronized_cache: (key -> 'a) -> key -> 'a
type set = int table
val add_set: key -> set -> set
val make_set: key list -> set
@@ -84,6 +85,8 @@
fun make_strict es = Table (Table.make es);
+val unsynchronized_cache = Table.unsynchronized_cache;
+
(* set with order of addition *)