--- a/src/Pure/General/table.ML Mon Nov 26 19:56:09 2012 +0100
+++ b/src/Pure/General/table.ML Mon Nov 26 20:09:51 2012 +0100
@@ -55,6 +55,8 @@
val make_list: (key * 'a) list -> 'a list table
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 make_set: key list -> set (*exception DUP*)
end;
functor Table(Key: KEY): TABLE =
@@ -394,6 +396,13 @@
fun merge_list eq = join (fn _ => Library.merge eq);
+(* unit tables *)
+
+type set = unit table;
+
+fun make_set entries = fold (fn x => update_new (x, ())) entries empty;
+
+
(* ML pretty-printing *)
val _ =