diff -r f084d599bb44 -r ad2899cdd528 src/Pure/cterm_items.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/cterm_items.ML	Thu Sep 09 15:45:27 2021 +0200
@@ -0,0 +1,38 @@
+(*  Title:      Pure/cterm_items.ML
+    Author:     Makarius
+
+Scalable collections of term items: for type thm and cterm.
+See als Pure/term_items.ML.
+*)
+
+structure Ctermtab:
+sig
+  include TABLE
+  val cterm_cache: (cterm -> 'a) -> cterm -> 'a
+end =
+struct
+
+structure Table = Table(type key = cterm val ord = Thm.fast_term_ord);
+open Table;
+
+fun cterm_cache f = Cache.create empty lookup update f;
+
+end;
+
+
+structure Thmtab:
+sig
+  include TABLE
+  val thm_cache: (thm -> 'a) -> thm -> 'a
+end =
+struct
+
+structure Table = Table(type key = thm val ord = Thm.thm_ord);
+open Table;
+
+fun thm_cache f = Cache.create empty lookup update f;
+
+end;
+
+
+structure Cterms: TERM_ITEMS = Term_Items(type key = cterm val ord = Thm.fast_term_ord);