# HG changeset patch
# User wenzelm
# Date 1517261107 -3600
# Node ID 37db2dc5c022539dee8ed6a6489471d18e5c706b
# Parent  ea029c521b5bf395f85f6df589efdfb69c24d43f
clarified operations;

diff -r ea029c521b5b -r 37db2dc5c022 src/Pure/General/table.ML
--- a/src/Pure/General/table.ML	Mon Jan 29 21:14:42 2018 +0100
+++ b/src/Pure/General/table.ML	Mon Jan 29 22:25:07 2018 +0100
@@ -57,6 +57,7 @@
   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 remove_set: key -> set -> set
   val make_set: key list -> set
 end;
 
@@ -406,7 +407,8 @@
 
 type set = unit table;
 
-fun insert_set x = update (x, ());
+fun insert_set x = default (x, ());
+fun remove_set x : set -> set = delete_safe x;
 fun make_set entries = fold insert_set entries empty;