src/HOL/Multivariate_Analysis/normarith.ML
changeset 40721 e5089e903e39
parent 40718 4d7211968607
child 42361 23f352990944
--- 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;