src/Pure/term_items.ML

--- a/src/Pure/term_items.ML	Thu Jul 18 11:02:08 2024 +0200
+++ b/src/Pure/term_items.ML	Thu Jul 18 11:36:09 2024 +0200
@@ -34,7 +34,7 @@
   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};
+  type 'a cache_ops = {apply: key -> 'a, reset: unit -> unit, size: unit -> int};
   val unsynchronized_cache: (key -> 'a) -> 'a cache_ops
   type set = int table
   val add_set: key -> set -> set