--- a/src/Pure/General/table.ML Mon Dec 11 19:36:28 2023 +0100
+++ b/src/Pure/General/table.ML Mon Dec 11 19:51:30 2023 +0100
@@ -41,6 +41,7 @@
val default: key * 'a -> 'a table -> 'a table
val map_entry: key -> ('a -> 'a) (*exception SAME*) -> 'a table -> 'a table
val map_default: key * 'a -> ('a -> 'a) -> 'a table -> 'a table
+ val make_distinct: (key * 'a) list -> 'a table
val make: (key * 'a) list -> 'a table (*exception DUP*)
val join: (key -> 'a * 'a -> 'a) (*exception SAME*) ->
'a table * 'a table -> 'a table (*exception DUP*)
@@ -531,6 +532,8 @@
(* simultaneous modifications *)
+fun make_distinct entries = build (fold default entries);
+
fun make entries = build (fold update_new entries);
fun join f (tab1, tab2) =