src/Pure/General/change_table.ML

   val map_default: key * 'a -> ('a -> 'a) -> 'a T -> 'a T
   val delete_safe: key -> 'a T -> 'a T
   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 =
 struct
 

   end;
 
 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 *)
 
 fun fold f arg = Table.fold f (table_of arg);
 fun dest arg = Table.dest (table_of arg);