# HG changeset patch
# User paulson
# Date 976699840 -3600
# Node ID 68f3fddd6e24a1ac8a93d02544059f446d9dc99f
# Parent  ddd33e0f4935bab1eeb1b27f66bdea12deae2cb9
tries harder to remove negative literals, e.g.
-2*x = 0 goes to x=0 rather than -x=0.

diff -r ddd33e0f4935 -r 68f3fddd6e24 src/Provers/Arith/cancel_numeral_factor.ML
--- 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 ()