# HG changeset patch
# User wenzelm
# Date 1702039007 -3600
# Node ID 8b77c95ed36af23baab275939056fc570abb1737
# Parent  2586c8b422ed1a7c907e700beee15a23025bfd52
more operations;

diff -r 2586c8b422ed -r 8b77c95ed36a src/Pure/term_items.ML
--- 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 *)