src/HOL/Library/positivstellensatz.ML
changeset 33002 f3f02f36a3e2
parent 32843 c8f5a7c8353f
child 33035 15eab423e573
child 33038 8f9594c31de4
     1.1 --- a/src/HOL/Library/positivstellensatz.ML	Mon Oct 19 16:47:21 2009 +0200
     1.2 +++ b/src/HOL/Library/positivstellensatz.ML	Mon Oct 19 21:54:57 2009 +0200
     1.3 @@ -83,8 +83,8 @@
     1.4   else
     1.5    let val mon1 = dest_monomial m1 
     1.6        val mon2 = dest_monomial m2
     1.7 -      val deg1 = fold (curry op + o snd) mon1 0
     1.8 -      val deg2 = fold (curry op + o snd) mon2 0 
     1.9 +      val deg1 = fold (Integer.add o snd) mon1 0
    1.10 +      val deg2 = fold (Integer.add o snd) mon2 0 
    1.11    in if deg1 < deg2 then GREATER else if deg1 > deg2 then LESS
    1.12       else list_ord (prod_ord cterm_ord int_ord) (mon1,mon2)
    1.13    end;