clarified operations;
authorwenzelm
Mon, 29 Jan 2018 22:25:07 +0100
changeset 67529 37db2dc5c022
parent 67528 ea029c521b5b
child 67530 a7de81d847b0
clarified operations;
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;