src/Pure/library.ML
changeset 33043 ff71cadefb14
parent 33040 cffdb7b28498
parent 33042 ddf1f03a9ad9
child 33050 fe166e8b9f07
     1.1 --- a/src/Pure/library.ML	Wed Oct 21 10:15:31 2009 +0200
     1.2 +++ b/src/Pure/library.ML	Wed Oct 21 12:08:52 2009 +0200
     1.3 @@ -157,12 +157,12 @@
     1.4    val insert: ('a * 'a -> bool) -> 'a -> 'a list -> 'a list
     1.5    val remove: ('b * 'a -> bool) -> 'b -> 'a list -> 'a list
     1.6    val update: ('a * 'a -> bool) -> 'a -> 'a list -> 'a list
     1.7 +  val union: ('a * 'a -> bool) -> 'a list -> 'a list -> 'a list
     1.8    val subtract: ('b * 'a -> bool) -> 'b list -> 'a list -> 'a list
     1.9    val merge: ('a * 'a -> bool) -> 'a list * 'a list -> 'a list
    1.10    val mem: ''a * ''a list -> bool
    1.11    val mem_int: int * int list -> bool
    1.12    val mem_string: string * string list -> bool
    1.13 -  val union: ('a * 'a -> bool) -> 'a list * 'a list -> 'a list
    1.14    val inter: ('a * 'b -> bool) -> 'a list * 'b list -> 'a list
    1.15    val subset: ('a * 'b -> bool) -> 'a list * 'b list -> bool
    1.16    val eq_set: ('a * 'b -> bool) -> 'a list * 'b list -> bool
    1.17 @@ -782,6 +782,7 @@
    1.18  fun remove eq x xs = if member eq xs x then filter_out (fn y => eq (x, y)) xs else xs;
    1.19  fun update eq x xs = cons x (remove eq x xs);
    1.20  
    1.21 +fun union eq = fold (insert eq);
    1.22  fun subtract eq = fold (remove eq);
    1.23  
    1.24  fun merge eq (xs, ys) =
    1.25 @@ -796,11 +797,6 @@
    1.26  fun (x: int) mem_int xs = member (op =) xs x;
    1.27  fun (x: string) mem_string xs = member (op =) xs x;
    1.28  
    1.29 -(*union of sets represented as lists: no repetitions*)
    1.30 -fun union eq (xs, []) = xs
    1.31 -  | union eq ([], ys) = ys
    1.32 -  | union eq (x :: xs, ys) = union eq (xs, insert eq x ys);
    1.33 -
    1.34  (*intersection*)
    1.35  fun inter eq ([], ys) = []
    1.36    | inter eq (x::xs, ys) =