src/Pure/library.ML
changeset 33038 8f9594c31de4
parent 33037 b22e44496dc2
child 33040 cffdb7b28498
child 33042 ddf1f03a9ad9
     1.1 --- a/src/Pure/library.ML	Tue Oct 20 16:13:01 2009 +0200
     1.2 +++ b/src/Pure/library.ML	Wed Oct 21 08:14:38 2009 +0200
     1.3 @@ -162,10 +162,10 @@
     1.4    val mem: ''a * ''a list -> bool
     1.5    val mem_int: int * int list -> bool
     1.6    val mem_string: string * string list -> bool
     1.7 -  val gen_union: ('a * 'a -> bool) -> 'a list * 'a list -> 'a list
     1.8 -  val gen_inter: ('a * 'b -> bool) -> 'a list * 'b list -> 'a list
     1.9 -  val gen_subset: ('a * 'b -> bool) -> 'a list * 'b list -> bool
    1.10 -  val gen_eq_set: ('a * 'b -> bool) -> 'a list * 'b list -> bool
    1.11 +  val union: ('a * 'a -> bool) -> 'a list * 'a list -> 'a list
    1.12 +  val inter: ('a * 'b -> bool) -> 'a list * 'b list -> 'a list
    1.13 +  val subset: ('a * 'b -> bool) -> 'a list * 'b list -> bool
    1.14 +  val eq_set: ('a * 'b -> bool) -> 'a list * 'b list -> bool
    1.15    val \ : ''a list * ''a -> ''a list
    1.16    val \\ : ''a list * ''a list -> ''a list
    1.17    val distinct: ('a * 'a -> bool) -> 'a list -> 'a list
    1.18 @@ -799,23 +799,23 @@
    1.19  fun (x: string) mem_string xs = member (op =) xs x;
    1.20  
    1.21  (*union of sets represented as lists: no repetitions*)
    1.22 -fun gen_union eq (xs, []) = xs
    1.23 -  | gen_union eq ([], ys) = ys
    1.24 -  | gen_union eq (x :: xs, ys) = gen_union eq (xs, insert eq x ys);
    1.25 +fun union eq (xs, []) = xs
    1.26 +  | union eq ([], ys) = ys
    1.27 +  | union eq (x :: xs, ys) = union eq (xs, insert eq x ys);
    1.28  
    1.29  (*intersection*)
    1.30 -fun gen_inter eq ([], ys) = []
    1.31 -  | gen_inter eq (x::xs, ys) =
    1.32 -      if member eq ys x then x :: gen_inter eq (xs, ys)
    1.33 -      else gen_inter eq (xs, ys);
    1.34 +fun inter eq ([], ys) = []
    1.35 +  | inter eq (x::xs, ys) =
    1.36 +      if member eq ys x then x :: inter eq (xs, ys)
    1.37 +      else inter eq (xs, ys);
    1.38  
    1.39  (*subset*)
    1.40 -fun gen_subset eq (xs, ys) = forall (member eq ys) xs;
    1.41 +fun subset eq (xs, ys) = forall (member eq ys) xs;
    1.42  
    1.43  (*set equality*)
    1.44 -fun gen_eq_set eq (xs, ys) =
    1.45 +fun eq_set eq (xs, ys) =
    1.46    eq_list eq (xs, ys) orelse
    1.47 -    (gen_subset eq (xs, ys) andalso gen_subset (eq o swap) (ys, xs));
    1.48 +    (subset eq (xs, ys) andalso subset (eq o swap) (ys, xs));
    1.49  
    1.50  
    1.51  (*removing an element from a list WITHOUT duplicates*)