# HG changeset patch
# User wenzelm
# Date 1290801141 -3600
# Node ID 4d72119686073c47dd173f48a4a8c068dfbc089b
# Parent  88f2955a111e0971250875b1fc13a0644a9ee718
eliminated some clones of eq_list;

diff -r 88f2955a111e -r 4d7211968607 src/HOL/Multivariate_Analysis/normarith.ML
--- a/src/HOL/Multivariate_Analysis/normarith.ML	Fri Nov 26 18:07:00 2010 +0100
+++ b/src/HOL/Multivariate_Analysis/normarith.ML	Fri Nov 26 20:52:21 2010 +0100
@@ -117,13 +117,6 @@
   [] => []
 | h::t => map (cons h) (combinations (k - 1) t) @ combinations k t
 
-
-fun forall2 p l1 l2 = case (l1,l2) of
-   ([],[]) => true
- | (h1::t1,h2::t2) => p h1 h2 andalso forall2 p t1 t2
- | _ => false;
-
-
 fun vertices vs eqs =
  let
   fun vertex cmb = case solve(vs,cmb) of
@@ -131,16 +124,16 @@
    | SOME soln => SOME (map (fn v => FuncUtil.Intfunc.tryapplyd soln v Rat.zero) vs)
   val rawvs = map_filter vertex (combinations (length vs) eqs)
   val unset = filter (forall (fn c => c >=/ Rat.zero)) rawvs
- in fold_rev (insert (uncurry (forall2 (curry op =/)))) unset []
+ in fold_rev (insert (eq_list op =/)) unset []
  end
 
-fun subsumes l m = forall2 (fn x => fn y => Rat.abs x <=/ Rat.abs y) l m
+val subsumes = eq_list (fn (x, y) => Rat.abs x <=/ Rat.abs y)
 
 fun subsume todo dun = case todo of
  [] => dun
 |v::ovs =>
-   let val dun' = if exists (fn w => subsumes w v) dun then dun
-                  else v::(filter (fn w => not(subsumes v w)) dun)
+   let val dun' = if exists (fn w => subsumes (w, v)) dun then dun
+                  else v:: filter (fn w => not (subsumes (v, w))) dun
    in subsume ovs dun'
    end;
 
diff -r 88f2955a111e -r 4d7211968607 src/HOL/Tools/groebner.ML
--- a/src/HOL/Tools/groebner.ML	Fri Nov 26 18:07:00 2010 +0100
+++ b/src/HOL/Tools/groebner.ML	Fri Nov 26 20:52:21 2010 +0100
@@ -233,14 +233,9 @@
 
 fun align  ((p,hp),(q,hq)) =
   if poly_lt p q then ((p,hp),(q,hq)) else ((q,hq),(p,hp));
-fun forall2 p l1 l2 =
-  case (l1,l2) of
-    ([],[]) => true
-  | (h1::t1,h2::t2) => p h1 h2 andalso forall2 p t1 t2
-  | _ => false;
 
 fun poly_eq p1 p2 =
-  forall2 (fn (c1,m1) => fn (c2,m2) => c1 =/ c2 andalso (m1: int list) = m2) p1 p2;
+  eq_list (fn ((c1, m1), (c2, m2)) => c1 =/ c2 andalso (m1: int list) = m2) (p1, p2);
 
 fun memx ((p1,h1),(p2,h2)) ppairs =
   not (exists (fn ((q1,_),(q2,_)) => poly_eq p1 q1 andalso poly_eq p2 q2) ppairs);