--- a/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML Fri Nov 26 21:31:46 2010 +0100
+++ b/src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML Fri Nov 26 22:04:33 2010 +0100
@@ -103,11 +103,6 @@
fun iszero (k,r) = r =/ rat_0;
-fun fold_rev2 f l1 l2 b =
- case (l1,l2) of
- ([],[]) => b
- | (h1::t1,h2::t2) => f h1 h2 (fold_rev2 f t1 t2 b)
- | _ => error "fold_rev2";
(* Vectors. Conventionally indexed 1..n. *)
--- a/src/HOL/Multivariate_Analysis/normarith.ML Fri Nov 26 21:31:46 2010 +0100
+++ b/src/HOL/Multivariate_Analysis/normarith.ML Fri Nov 26 22:04:33 2010 +0100
@@ -239,10 +239,6 @@
Const(@{const_name norm},_)$_ => arg_conv vector_canon_conv ct
| _ => raise CTERM ("norm_canon_conv", [ct])
-fun fold_rev2 f [] [] z = z
- | fold_rev2 f (x::xs) (y::ys) z = f x y (fold_rev2 f xs ys z)
- | fold_rev2 f _ _ _ = raise UnequalLengths;
-
fun int_flip v eq =
if FuncUtil.Intfunc.defined eq v
then FuncUtil.Intfunc.update (v, Rat.neg (FuncUtil.Intfunc.apply eq v)) eq else eq;
--- a/src/Pure/library.ML Fri Nov 26 21:31:46 2010 +0100
+++ b/src/Pure/library.ML Fri Nov 26 22:04:33 2010 +0100
@@ -97,6 +97,7 @@
val eq_list: ('a * 'b -> bool) -> 'a list * 'b list -> bool
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 zip_options: 'a list -> 'b option list -> ('a * 'b) list
val ~~ : 'a list * 'b list -> ('a * 'b) list
@@ -544,6 +545,10 @@
| fold2 f (x :: xs) (y :: ys) z = fold2 f xs ys (f x y z)
| fold2 f _ _ _ = raise UnequalLengths;
+fun fold_rev2 f [] [] z = z
+ | fold_rev2 f (x :: xs) (y :: ys) z = f x y (fold_rev2 f xs ys z)
+ | fold_rev2 f _ _ _ = raise UnequalLengths;
+
fun forall2 P [] [] = true
| forall2 P (x :: xs) (y :: ys) = P x y andalso forall2 P xs ys
| forall2 P _ _ = false;