--- 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 *)
--- 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 *)