clarified Table.make_set: duplicate arguments are allowed, like Table.make_list or Scala Set() formation;

--- a/src/Pure/General/table.ML	Mon Nov 17 18:19:06 2014 +0100
+++ b/src/Pure/General/table.ML	Tue Nov 18 20:56:34 2014 +0100
@@ -56,7 +56,7 @@
   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*)
+  val make_set: key list -> set
 end;
 
 functor Table(Key: KEY): TABLE =
@@ -405,7 +405,7 @@
 
 type set = unit table;
 
-fun make_set entries = fold (fn x => update_new (x, ())) entries empty;
+fun make_set entries = fold (fn x => update (x, ())) entries empty;
 
 
 (* ML pretty-printing *)