# HG changeset patch
# User wenzelm
# Date 1353956991 -3600
# Node ID c97c5c34fb1de09141788e42cf397f5894846561
# Parent  eef21a0726f153153bd21f80572e52238ebd4e4f
convenience operations for table as set;

diff -r eef21a0726f1 -r c97c5c34fb1d src/Pure/General/table.ML
--- 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 _ =