# HG changeset patch
# User wenzelm
# Date 1290805473 -3600
# Node ID e5089e903e394b7c70991ca58d70e95c46883e9f
# Parent  b770df486e5cdfe70f70587a54e1d46fecfc2552
just one version of fold_rev2;

diff -r b770df486e5c -r e5089e903e39 src/HOL/Library/Sum_Of_Squares/sum_of_squares.ML
--- 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.                                     *)
 
diff -r b770df486e5c -r e5089e903e39 src/HOL/Multivariate_Analysis/normarith.ML
--- 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;
diff -r b770df486e5c -r e5089e903e39 src/Pure/library.ML
--- 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;