# HG changeset patch
# User wenzelm
# Date 1468619227 -7200
# Node ID 1c2c045decb361b6b4dd98ca49d1b5c25fe22c6c
# Parent  0fc8be2f8176d8588ef9d9a32f52fdbb549e4564
more operations;

diff -r 0fc8be2f8176 -r 1c2c045decb3 src/Pure/General/table.ML
--- a/src/Pure/General/table.ML	Fri Jul 15 23:46:28 2016 +0200
+++ b/src/Pure/General/table.ML	Fri Jul 15 23:47:07 2016 +0200
@@ -56,6 +56,7 @@
   val dest_list: 'a list table -> (key * 'a) list
   val merge_list: ('a * 'a -> bool) -> 'a list table * 'a list table -> 'a list table
   type set = unit table
+  val insert_set: key -> set -> set
   val make_set: key list -> set
 end;
 
@@ -405,7 +406,8 @@
 
 type set = unit table;
 
-fun make_set entries = fold (fn x => update (x, ())) entries empty;
+fun insert_set x = update (x, ());
+fun make_set entries = fold insert_set entries empty;
 
 
 (* ML pretty-printing *)