# HG changeset patch
# User wenzelm
# Date 1681211203 -7200
# Node ID 353c4d3e6dda249e240392577b897028b8d986b1
# Parent  d1d28b36ba59b8002e104de544d3eaf1dd5b1289
more operations;

diff -r d1d28b36ba59 -r 353c4d3e6dda src/Pure/General/set.ML
--- a/src/Pure/General/set.ML	Tue Apr 11 11:28:57 2023 +0200
+++ b/src/Pure/General/set.ML	Tue Apr 11 13:06:43 2023 +0200
@@ -27,6 +27,7 @@
   val insert: elem -> T -> T
   val make: elem list -> T
   val merge: T * T -> T
+  val merges: T list -> T
   val remove: elem -> T -> T
   val subtract: T -> T -> T
 end;
@@ -343,6 +344,9 @@
 
 fun make elems = build (fold insert elems);
 
+
+(* merge *)
+
 fun merge (set1, set2) =
   if pointer_eq (set1, set2) then set1
   else if is_empty set1 then set2
@@ -351,6 +355,8 @@
   then fold_set insert set2 set1
   else fold_set insert set1 set2;
 
+fun merges sets = Library.foldl merge (empty, sets);
+
 
 (* remove *)
 
diff -r d1d28b36ba59 -r 353c4d3e6dda src/Pure/General/table.ML
--- a/src/Pure/General/table.ML	Tue Apr 11 11:28:57 2023 +0200
+++ b/src/Pure/General/table.ML	Tue Apr 11 13:06:43 2023 +0200
@@ -45,6 +45,9 @@
   val join: (key -> 'a * 'a -> 'a) (*exception SAME*) ->
     'a table * 'a table -> 'a table                                    (*exception DUP*)
   val merge: ('a * 'a -> bool) -> 'a table * 'a table -> 'a table      (*exception DUP*)
+  val joins: (key -> 'a * 'a -> 'a) (*exception SAME*) ->
+    'a table list -> 'a table                                          (*exception DUP*)
+  val merges: ('a * 'a -> bool) -> 'a table list -> 'a table           (*exception DUP*)
   val delete: key -> 'a table -> 'a table                              (*exception UNDEF*)
   val delete_safe: key -> 'a table -> 'a table
   val member: ('b * 'a -> bool) -> 'a table -> key * 'b -> bool
@@ -591,6 +594,9 @@
 
 fun merge eq = join (fn key => fn xy => if eq xy then raise SAME else raise DUP key);
 
+fun joins f tabs = Library.foldl (join f) (empty, tabs);
+fun merges eq tabs = Library.foldl (merge eq) (empty, tabs);
+
 
 (* list tables *)