src/Pure/library.ML

   exception UnequalLengths
   val cons: 'a -> 'a list -> 'a list
   val single: 'a -> 'a list
   val append: 'a list -> 'a list -> 'a list
   val apply: ('a -> 'a) list -> 'a -> 'a
-  val foldr1: ('a * 'a -> 'a) -> 'a list -> 'a
   val fold: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
   val fold_rev: ('a -> 'b -> 'b) -> 'a list -> 'b -> 'b
   val foldl_map: ('a * 'b -> 'a * 'c) -> 'a * 'b list -> 'a * 'c list
+  val foldr1: ('a * 'a -> 'a) -> 'a list -> 'a
   val foldln: ('a * int -> 'b -> 'b) -> 'a list -> 'b -> 'b
   val unflat: 'a list list -> 'b list -> 'b list list
   val splitAt: int * 'a list -> 'a list * 'a list
   val dropwhile: ('a -> bool) -> 'a list -> 'a list
   val map_nth_elem: int -> ('a -> 'a) -> 'a list -> 'a list

   val gen_mem: ('a * 'b -> bool) -> 'a * 'b list -> bool
   val ins: ''a * ''a list -> ''a list
   val ins_int: int * int list -> int list
   val ins_string: string * string list -> string list
   val gen_ins: ('a * 'a -> bool) -> 'a * 'a list -> 'a list
+  val insert: ('a * 'a -> bool) -> 'a -> 'a list -> 'a list
+  val remove: ('a * 'a -> bool) -> 'a -> 'a list -> 'a list
   val union: ''a list * ''a list -> ''a list
   val union_int: int list * int list -> int list
   val union_string: string list * string list -> string list
   val gen_union: ('a * 'a -> bool) -> 'a list * 'a list -> 'a list
   val gen_inter: ('a * 'b -> bool) -> 'a list * 'b list -> 'a list

   val gen_subset: ('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
   val gen_rems: ('a * 'b -> bool) -> 'a list * 'b list -> 'a list
-  val gen_remove: ('a * 'b -> bool) -> 'b -> 'a list -> 'a list
-  val remove: ''a -> ''a list -> ''a list
   val gen_distinct: ('a * 'a -> bool) -> 'a list -> 'a list
   val distinct: ''a list -> ''a list
   val findrep: ''a list -> ''a list
   val gen_duplicates: ('a * 'a -> bool) -> 'a list -> 'a list
   val duplicates: ''a list -> ''a list

 fun cons x xs = x :: xs;
 fun single x = [x];
 
 fun append xs ys = xs @ ys;
 
-(* tail recursive version *)
-fun rev_append xs ys = List.revAppend(xs,ys);
+fun rev_append xs ys = List.revAppend (xs, ys);
 
 fun apply [] x = x
   | apply (f :: fs) x = apply fs (f x);
 
 
 (* fold *)
+
+fun fold _ [] y = y
+  | fold f (x :: xs) y = fold f xs (f x y);
+
+fun fold_rev _ [] y = y
+  | fold_rev f (x :: xs) y = f x (fold_rev f xs y);
+
+fun foldl_map _ (x, []) = (x, [])
+  | foldl_map f (x, y :: ys) =
+      let
+        val (x', y') = f (x, y);
+        val (x'', ys') = foldl_map f (x', ys);
+      in (x'', y' :: ys') end;
 
 (*the following versions of fold are designed to fit nicely with infixes*)
 
 (*  (op @) (e, [x1, ..., xn])  ===>  ((e @ x1) @ x2) ... @ xn
     for operators that associate to the left (TAIL RECURSIVE)*)

 fun foldr1 f l =
   let fun itr [x] = x
         | itr (x::l) = f(x, itr l)
   in  itr l  end;
 
-fun fold f xs y = foldl (fn (y', x) => f x y') (y, xs);
-fun fold_rev f xs y = foldr (fn (x, y') => f x y') (xs, y);
-
-fun foldl_map _ (x, []) = (x, [])
-  | foldl_map f (x, y :: ys) =
-      let
-        val (x', y') = f (x, y);
-        val (x'', ys') = foldl_map f (x', ys);
-      in (x'', y' :: ys') end;
-
 fun foldln f xs e = fst (foldl (fn ((e,i), x) => (f (x,i) e, i+1)) ((e,1),xs));
+
 
 (* basic list functions *)
 
 (*take the first n elements from a list*)
 fun take (n, []) = []

 
 (*generalized membership test*)
 fun gen_mem eq (x, []) = false
   | gen_mem eq (x, y :: ys) = eq (x, y) orelse gen_mem eq (x, ys);
 
+(*insert and remove*)
+fun insert eq x xs = if gen_mem eq (x, xs) then xs else x :: xs;
+fun remove eq x xs = if gen_mem eq (x, xs) then filter_out (fn y => eq (x, y)) xs else xs;
 
 (*insertion into list if not already there*)
 fun (x ins xs) = if x mem xs then xs else x :: xs;
 
 (*insertion into list, optimized version for ints*)

 
 (*insertion into list, optimized version for strings*)
 fun (x ins_string xs) = if x mem_string xs then xs else x :: xs;
 
 (*generalized insertion*)
-fun gen_ins eq (x, xs) = if gen_mem eq (x, xs) then xs else x :: xs;
-
+fun gen_ins eq (x, xs) = insert eq x xs;
 
 (*union of sets represented as lists: no repetitions*)
 fun xs union [] = xs
   | [] union ys = ys
   | (x :: xs) union ys = xs union (x ins ys);

 fun ys \\ xs = foldl (op \) (ys,xs);
 
 (*removing an element from a list -- possibly WITH duplicates*)
 fun gen_rem eq (xs, y) = filter_out (fn x => eq (x, y)) xs;
 fun gen_rems eq (xs, ys) = filter_out (fn x => gen_mem eq (x, ys)) xs;
-
-fun gen_remove eq x xs = gen_rem eq (xs, x);
-fun remove x xs = gen_rem (op =) (xs, x);
 
 (*makes a list of the distinct members of the input; preserves order, takes
   first of equal elements*)
 fun gen_distinct eq lst =
   let