--- a/src/Provers/Arith/cancel_numeral_factor.ML Wed Dec 13 10:11:13 2000 +0100
+++ b/src/Provers/Arith/cancel_numeral_factor.ML Wed Dec 13 10:30:40 2000 +0100
@@ -61,7 +61,8 @@
val (m1, t1') = Data.dest_coeff t1
and (m2, t2') = Data.dest_coeff t2
val d = (*if both are negative, also divide through by ~1*)
- if m1<0 andalso m2<0 then ~ (gcd(m1,m2)) else gcd(m1,m2)
+ if (m1<0 andalso m2<=0) orelse
+ (m1<=0 andalso m2<0) then ~ (gcd(m1,m2)) else gcd(m1,m2)
val _ = if d=1 then (*trivial, so do nothing*)
raise TERM("cancel_numeral_factor", [])
else ()