more operations;
tuned;

--- a/src/Pure/General/change_table.ML	Fri May 05 23:50:31 2023 +0200
+++ b/src/Pure/General/change_table.ML	Sat May 06 13:42:03 2023 +0200
@@ -33,6 +33,7 @@
   val insert_list: ('a * 'a -> bool) -> key * 'a -> 'a list T -> 'a list T
   val remove_list: ('b * 'a -> bool) -> key * 'b -> 'a list T -> 'a list T
   val update_list: ('a * 'a -> bool) -> key * 'a -> 'a list T -> 'a list T
+  val merge_list: ('a * 'a -> bool) -> 'a list T * 'a list T -> 'a list T
 end;
 
 functor Change_Table(Key: KEY): CHANGE_TABLE =
@@ -138,6 +139,9 @@
 fun merge eq =
   join (fn key => fn xy => if eq xy then raise Table.SAME else raise Table.DUP key);
 
+fun merge_list eq =
+  join (fn _ => fn xy => if eq_list eq xy then raise Table.SAME else Library.merge eq xy);
+
 
 (* derived operations *)
 

--- a/src/Pure/General/table.ML	Fri May 05 23:50:31 2023 +0200
+++ b/src/Pure/General/table.ML	Sat May 06 13:42:03 2023 +0200
@@ -635,7 +635,7 @@
 fun make_list args = build (fold_rev cons_list args);
 fun dest_list tab = maps (fn (key, xs) => map (pair key) xs) (dest tab);
 fun merge_list eq =
-  join (fn _ => fn args => if eq_list eq args then raise SAME else Library.merge eq args);
+  join (fn _ => fn xy => if eq_list eq xy then raise SAME else Library.merge eq xy);
 
 
 (* set operations *)