# HG changeset patch # User wenzelm # Date 1683373323 -7200 # Node ID a7ca67369755173c9c6f2cbf8345298fbc229ec6 # Parent 93999ffdb9dd7f81ebc06101bed38ad9b6f40ee7 more operations; tuned; diff -r 93999ffdb9dd -r a7ca67369755 src/Pure/General/change_table.ML --- 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 *) diff -r 93999ffdb9dd -r a7ca67369755 src/Pure/General/table.ML --- 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 *)