clarified Table.make_set: duplicate arguments are allowed, like Table.make_list or Scala Set() formation;
authorwenzelm
Tue Nov 18 20:56:34 2014 +0100 (2014-11-18)
changeset 59012f4e9bd04e1d5
parent 59011 4902a2fec434
child 59013 f319054e8dff
clarified Table.make_set: duplicate arguments are allowed, like Table.make_list or Scala Set() formation;
src/Pure/General/table.ML
     1.1 --- a/src/Pure/General/table.ML	Mon Nov 17 18:19:06 2014 +0100
     1.2 +++ b/src/Pure/General/table.ML	Tue Nov 18 20:56:34 2014 +0100
     1.3 @@ -56,7 +56,7 @@
     1.4    val dest_list: 'a list table -> (key * 'a) list
     1.5    val merge_list: ('a * 'a -> bool) -> 'a list table * 'a list table -> 'a list table
     1.6    type set = unit table
     1.7 -  val make_set: key list -> set                                        (*exception DUP*)
     1.8 +  val make_set: key list -> set
     1.9  end;
    1.10  
    1.11  functor Table(Key: KEY): TABLE =
    1.12 @@ -405,7 +405,7 @@
    1.13  
    1.14  type set = unit table;
    1.15  
    1.16 -fun make_set entries = fold (fn x => update_new (x, ())) entries empty;
    1.17 +fun make_set entries = fold (fn x => update (x, ())) entries empty;
    1.18  
    1.19  
    1.20  (* ML pretty-printing *)