# HG changeset patch
# User wenzelm
# Date 1701714279 -3600
# Node ID 6a84d18fa548da2e4db2630719cd29899e97ed11
# Parent  45b2171e9e034b29870ebdca045818fe455c52f0
more operations;
tuned semicolons;

diff -r 45b2171e9e03 -r 6a84d18fa548 src/Pure/cterm_items.ML
--- a/src/Pure/cterm_items.ML	Mon Dec 04 12:10:39 2023 +0100
+++ b/src/Pure/cterm_items.ML	Mon Dec 04 19:24:39 2023 +0100
@@ -33,7 +33,7 @@
 structure Term_Items = Term_Items
 (
   type key = cterm;
-  val ord = Thm.fast_term_ord
+  val ord = Thm.fast_term_ord;
 );
 open Term_Items;
 
diff -r 45b2171e9e03 -r 6a84d18fa548 src/Pure/term_items.ML
--- a/src/Pure/term_items.ML	Mon Dec 04 12:10:39 2023 +0100
+++ b/src/Pure/term_items.ML	Mon Dec 04 19:24:39 2023 +0100
@@ -25,6 +25,8 @@
   val get_first: (key * 'a -> 'b option) -> 'a table -> 'b option
   val lookup: 'a table -> key -> 'a option
   val defined: 'a table -> key -> bool
+  val update: key * 'a -> 'a table -> 'a table
+  val remove: key -> 'a table -> 'a table
   val add: key * 'a -> 'a table -> 'a table
   val make: (key * 'a) list -> 'a table
   val make1: key * 'a -> 'a table
@@ -70,6 +72,9 @@
 fun lookup (Table tab) = Table.lookup tab;
 fun defined (Table tab) = Table.defined tab;
 
+fun update e (Table tab) = Table (Table.update e tab);
+fun remove x (Table tab) = Table (Table.delete_safe x tab);
+
 fun add entry (Table tab) = Table (Table.default entry tab);
 fun make es = build (fold add es);
 fun make1 e = build (add e);
@@ -178,7 +183,7 @@
 structure Term_Items = Term_Items
 (
   type key = indexname * typ;
-  val ord = pointer_eq_ord (prod_ord Term_Ord.fast_indexname_ord Term_Ord.typ_ord)
+  val ord = pointer_eq_ord (prod_ord Term_Ord.fast_indexname_ord Term_Ord.typ_ord);
 );
 open Term_Items;
 
@@ -199,7 +204,7 @@
 structure Term_Items = Term_Items
 (
   type key = string;
-  val ord = fast_string_ord
+  val ord = fast_string_ord;
 );
 open Term_Items;