# HG changeset patch
# User wenzelm
# Date 1142939889 -3600
# Node ID ce99525202fcbb58491e294bc468b8b8ddb32b60
# Parent  7689f81f89965598cbf40edef6944b6d9b40d196
added subtract;
tuned;

diff -r 7689f81f8996 -r ce99525202fc src/Pure/library.ML
--- a/src/Pure/library.ML	Tue Mar 21 12:18:07 2006 +0100
+++ b/src/Pure/library.ML	Tue Mar 21 12:18:09 2006 +0100
@@ -191,6 +191,7 @@
   val member: ('b * 'a -> bool) -> 'a list -> 'b -> bool
   val insert: ('a * 'a -> bool) -> 'a -> 'a list -> 'a list
   val remove: ('b * 'a -> bool) -> 'b -> 'a list -> 'a list
+  val subtract: ('b * 'a -> bool) -> 'b list -> 'a list -> 'a list
   val merge: ('a * 'a -> bool) -> 'a list * 'a list -> 'a list
   val mem: ''a * ''a list -> bool
   val mem_int: int * int list -> bool
@@ -212,6 +213,7 @@
   val eq_set: ''a list * ''a list -> bool
   val eq_set_string: string list * string list -> bool
   val gen_subset: ('a * 'b -> bool) -> 'a list * 'b list -> bool
+  val gen_eq_set: ('a * 'b -> bool) -> 'a list * 'b list -> bool
   val \ : ''a list * ''a -> ''a list
   val \\ : ''a list * ''a list -> ''a list
   val gen_rem: ('a * 'b -> bool) -> 'a list * 'b -> 'a list
@@ -877,7 +879,7 @@
   | space_explode sep str =
       let
         fun expl chs =
-          (case take_prefix (not_equal sep) chs of
+          (case take_prefix (fn s => s <> sep) chs of
             (cs, []) => [implode cs]
           | (cs, _ :: cs') => implode cs :: expl cs');
       in expl (explode str) end;
@@ -896,7 +898,7 @@
           let val d = tab_width - (pos mod tab_width) in (pos + d, replicate d " ") end
       | untab (pos, c) = (pos + 1, [c]);
   in
-    if not (exists (equal "\t") chs) then chs
+    if not (exists (fn c => c = "\t") chs) then chs
     else flat (#2 (foldl_map untab (0, chs)))
   end;
 
@@ -931,6 +933,8 @@
 fun insert eq x xs = if member eq xs x then xs else x :: xs;
 fun remove eq x xs = if member eq xs x then filter_out (fn y => eq (x, y)) xs else xs;
 
+fun subtract eq = fold (remove eq);
+
 fun merge _ ([], ys) = ys
   | merge eq (xs, ys) = fold_rev (insert eq) ys xs;
 
@@ -1009,6 +1013,10 @@
 
 fun gen_subset eq (xs, ys) = forall (member eq ys) xs;
 
+fun gen_eq_set eq (xs, ys) =
+  equal_lists eq (xs, ys) orelse
+    (gen_subset eq (xs, ys) andalso gen_subset (eq o swap) (ys, xs));
+
 
 (*removing an element from a list WITHOUT duplicates*)
 fun (y :: ys) \ x = if x = y then ys else y :: (ys \ x)