tries harder to remove negative literals, e.g.
-2*x = 0 goes to x=0 rather than -x=0.

--- 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 ()