src/Pure/term_items.ML

   val make1: key * 'a -> 'a table
   val make2: key * 'a -> key * 'a -> 'a table
   val make3: key * 'a -> key * 'a -> key * 'a -> 'a table
   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
   type set = int table
   val add_set: key -> set -> set
   val make_set: key list -> set
   val make1_set: key -> set
   val make2_set: key -> key -> set

 fun make2 e1 e2 = build (add e1 #> add e2);
 fun make3 e1 e2 e3 = build (add e1 #> add e2 #> add e3);
 
 type 'a cache_ops = 'a Table.cache_ops;
 val unsynchronized_cache = Table.unsynchronized_cache;
+val apply_unsynchronized_cache = Table.apply_unsynchronized_cache;
 
 
 (* set with order of addition *)
 
 type set = int table;