# HG changeset patch
# User wenzelm
# Date 1702320690 -3600
# Node ID 718798653cf1819b0c361bc480dc725064aac415
# Parent  288229384ed7943402b3e4a6041b5d46546da5dd
more operations;

diff -r 288229384ed7 -r 718798653cf1 src/Pure/General/table.ML
--- 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) =