eliminated some exotic combinators;

--- a/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Wed Oct 08 17:09:07 2014 +0200
+++ b/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Wed Oct 08 17:37:20 2014 +0200
@@ -134,7 +134,7 @@
 
 fun vector_of_list l =
   let val n = length l in
-    (n, fold_rev2 (curry FuncUtil.Intfunc.update) (1 upto n) l FuncUtil.Intfunc.empty): vector
+    (n, fold_rev FuncUtil.Intfunc.update (1 upto n ~~ l) FuncUtil.Intfunc.empty): vector
   end;
 
 (* Matrices; again rows and columns indexed from 1.                          *)
@@ -592,8 +592,8 @@
     (space_implode " " (map string_of_int blocksizes)) ^
     "\n" ^
     sdpa_of_vector obj ^
-    fold_rev2 (fn k => fn m => fn a => sdpa_of_blockdiagonal (k - 1) m ^ a)
-      (1 upto length mats) mats ""
+    fold_rev (fn (k, m) => fn a => sdpa_of_blockdiagonal (k - 1) m ^ a)
+      (1 upto length mats ~~ mats) ""
   end;
 
 (* Run prover on a problem in block diagonal form.                       *)
@@ -683,9 +683,9 @@
     val (_(*idmonlist*),ids) =  split_list (map2 mk_idmultiplier (1 upto length eqs) eqs)
     val blocksizes = map length sqmonlist
     val bigsum =
-      fold_rev2 (fn p => fn q => fn a => tri_epoly_pmul p q a) eqs ids
-        (fold_rev2 (fn (p,_) => fn s => fn a => tri_epoly_pmul p s a) monoid sqs
-          (epoly_of_poly(poly_neg pol)))
+      fold_rev (fn (p, q) => fn a => tri_epoly_pmul p q a) (eqs ~~ ids)
+        (fold_rev (fn ((p, _), s) => fn a => tri_epoly_pmul p s a) (monoid ~~ sqs)
+          (epoly_of_poly (poly_neg pol)))
     val eqns = FuncUtil.Monomialfunc.fold (fn (_, e) => fn a => e :: a) bigsum []
     val (pvs, assig) = tri_eliminate_all_equations (0, 0, 0) eqns
     val qvars = (0, 0, 0) :: pvs
@@ -753,7 +753,7 @@
     fun eval_sq sqs = fold_rev (fn (c, q) => poly_add (poly_cmul c (poly_mul q q))) sqs poly_0
     val sanity =
       fold_rev (fn ((p, _), s) => poly_add (poly_mul p (eval_sq s))) msq
-        (fold_rev2 (fn p => fn q => poly_add (poly_mul p q)) cfs eqs (poly_neg pol))
+        (fold_rev (fn (p, q) => poly_add (poly_mul p q)) (cfs ~~ eqs) (poly_neg pol))
   in
     if not(FuncUtil.Monomialfunc.is_empty sanity) then raise Sanity
     else (cfs, map (fn (a, b) => (snd a, b)) msq)

--- a/src/HOL/Multivariate_Analysis/normarith.ML	Wed Oct 08 17:09:07 2014 +0200
+++ b/src/HOL/Multivariate_Analysis/normarith.ML	Wed Oct 08 17:37:20 2014 +0200
@@ -295,7 +295,7 @@
        val rawverts = vertices nvs constraints
        fun check_solution v =
         let
-          val f = fold_rev2 (curry FuncUtil.Intfunc.update) nvs v (FuncUtil.Intfunc.onefunc (0, Rat.one))
+          val f = fold_rev FuncUtil.Intfunc.update (nvs ~~ v) (FuncUtil.Intfunc.onefunc (0, Rat.one))
         in forall (fn e => evaluate f e =/ Rat.zero) flippedequations
         end
        val goodverts = filter check_solution rawverts

--- a/src/Pure/Isar/code.ML	Wed Oct 08 17:09:07 2014 +0200
+++ b/src/Pure/Isar/code.ML	Wed Oct 08 17:37:20 2014 +0200
@@ -545,7 +545,7 @@
       else bad_thm ("Projection mismatch: " ^ quote rep_const ^ " vs. " ^ quote rep');
     val _ = check_eqn thy { allow_nonlinear = false,
       allow_consts = false, allow_pats = false } thm (lhs, rhs);
-    val _ = if forall2 (fn T => fn (_, sort) => Sign.of_sort thy (T, sort)) Ts vs' then ()
+    val _ = if ListPair.all (fn (T, (_, sort)) => Sign.of_sort thy (T, sort)) (Ts, vs') then ()
       else error ("Type arguments do not satisfy sort constraints of abstype certificate.");
   in (thm, tyco) end;
 

--- a/src/Pure/library.ML	Wed Oct 08 17:09:07 2014 +0200
+++ b/src/Pure/library.ML	Wed Oct 08 17:37:20 2014 +0200
@@ -101,8 +101,6 @@
   val fold_product: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c
   val map2: ('a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list
   val fold2: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c
-  val fold_rev2: ('a -> 'b -> 'c -> 'c) -> 'a list -> 'b list -> 'c -> 'c
-  val forall2: ('a -> 'b -> bool) -> 'a list -> 'b list -> bool
   val map_split: ('a -> 'b * 'c) -> 'a list -> 'b list * 'c list
   val zip_options: 'a list -> 'b option list -> ('a * 'b) list
   val ~~ : 'a list * 'b list -> ('a * 'b) list
@@ -535,14 +533,6 @@
   | fold2 f (x :: xs) (y :: ys) z = fold2 f xs ys (f x y z)
   | fold2 _ _ _ _ = raise ListPair.UnequalLengths;
 
-fun fold_rev2 _ [] [] z = z
-  | fold_rev2 f (x :: xs) (y :: ys) z = f x y (fold_rev2 f xs ys z)
-  | fold_rev2 _ _ _ _ = raise ListPair.UnequalLengths;
-
-fun forall2 _ [] [] = true
-  | forall2 P (x :: xs) (y :: ys) = P x y andalso forall2 P xs ys
-  | forall2 _ _ _ = raise ListPair.UnequalLengths;
-
 fun map_split _ [] = ([], [])
   | map_split f (x :: xs) =
       let