1.1 --- a/src/Tools/isac/Knowledge/GCD_Poly_ML.thy	Mon Sep 16 10:46:51 2013 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/GCD_Poly_ML.thy	Mon Sep 16 11:28:43 2013 +0200
     1.3 @@ -658,14 +658,14 @@
     1.4  
     1.5  subsection {* gcd_poly algorithm, code for [1] p.95 *}
     1.6  ML {*
     1.7 -  fun gcd_monom (c1, es1) (c2, es2) = (Integer.gcd c1 c2, map2 Integer.min es1 es2)
     1.8 +  fun gcd_monom (c1, es1) (c2, es2) = (Integer.gcd c1 c2, map2 Integer.min es1 es2) 
     1.9  
    1.10    (* naming of n, M, m, r, ...  follows Winkler p. 95 
    1.11      assumes: n = length es1 = length es2
    1.12      r: *)
    1.13 -  fun gcd_poly' a [monom as (c, es)] _ _ = [fold gcd_monom a monom]
    1.14 -    | gcd_poly' [monom as (c, es)] b _ _ = [fold gcd_monom b monom]
    1.15 -    | gcd_poly' (a as (_, es1)::_ : poly) (b as (_, es2)::_ : poly) n r =
    1.16 +  fun gcd_poly' a [monom as (c, es)] _ _ = [fold gcd_monom a monom] 
    1.17 +    | gcd_poly' [monom as (c, es)] b _ _ = [fold gcd_monom b monom] 
    1.18 +    | gcd_poly' (a as (_, es1)::_ : poly) (b as (_, es2)::_ : poly) n r = 
    1.19        if lex_ord (lmonom b) (lmonom a) then gcd_poly' b a n r else
    1.20          if n > 1
    1.21          then