# HG changeset patch
# User wenzelm
# Date 1682104346 -7200
# Node ID 38d0a90e87c156638e5be8c417e8d6d220e128bf
# Parent  01d6b2a44df8070325c0ca0fdfaa9f5c126f4233
more operations;

diff -r 01d6b2a44df8 -r 38d0a90e87c1 src/Pure/cterm_items.ML
--- a/src/Pure/cterm_items.ML	Fri Apr 21 18:53:25 2023 +0200
+++ b/src/Pure/cterm_items.ML	Fri Apr 21 21:12:26 2023 +0200
@@ -19,6 +19,8 @@
 
 end;
 
+structure Ctermset = Set(Ctermtab.Key);
+
 
 structure Cterms:
 sig
@@ -54,3 +56,5 @@
 fun thm_cache f = Cache.create empty lookup update f;
 
 end;
+
+structure Thmset = Set(Thmtab.Key);