src/Pure/library.ML
changeset 33049 c38f02fdf35d
parent 33040 cffdb7b28498
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:09:37 2009 +0200
     1.3 @@ -158,12 +158,12 @@
     1.4    val remove: ('b * 'a -> bool) -> 'b -> 'a list -> 'a list
     1.5    val update: ('a * 'a -> bool) -> 'a -> 'a list -> 'a list
     1.6    val subtract: ('b * 'a -> bool) -> 'b list -> 'a list -> 'a list
     1.7 +  val inter: ('a * 'b -> bool) -> 'b list -> 'a list -> 'a list
     1.8    val merge: ('a * 'a -> bool) -> 'a list * 'a list -> 'a list
     1.9    val mem: ''a * ''a list -> bool
    1.10    val mem_int: int * int list -> bool
    1.11    val mem_string: string * string list -> bool
    1.12    val union: ('a * 'a -> bool) -> 'a list * 'a list -> 'a list
    1.13 -  val inter: ('a * 'b -> bool) -> 'a list * 'b list -> 'a list
    1.14    val subset: ('a * 'b -> bool) -> 'a list * 'b list -> bool
    1.15    val eq_set: ('a * 'b -> bool) -> 'a list * 'b list -> bool
    1.16    val distinct: ('a * 'a -> bool) -> 'a list -> 'a list
    1.17 @@ -782,6 +782,8 @@
    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 inter eq xs = filter (member eq xs);
    1.22 +
    1.23  fun subtract eq = fold (remove eq);
    1.24  
    1.25  fun merge eq (xs, ys) =
    1.26 @@ -801,12 +803,6 @@
    1.27    | union eq ([], ys) = ys
    1.28    | union eq (x :: xs, ys) = union eq (xs, insert eq x ys);
    1.29  
    1.30 -(*intersection*)
    1.31 -fun inter eq ([], ys) = []
    1.32 -  | inter eq (x::xs, ys) =
    1.33 -      if member eq ys x then x :: inter eq (xs, ys)
    1.34 -      else inter eq (xs, ys);
    1.35 -
    1.36  (*subset*)
    1.37  fun subset eq (xs, ys) = forall (member eq ys) xs;
    1.38