--- 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;