src/HOL/Tools/groebner.ML

 
 fun dest_binary ct ct' =
   if is_binop ct ct' then Thm.dest_binop ct'
   else raise CTERM ("dest_binary: bad binop", [ct, ct'])
 
-val minus_rat = Rat.neg;
 val denominator_rat = Rat.dest #> snd #> Rat.of_int;
 fun int_of_rat a =
     case Rat.dest a of (i,1) => i | _ => error "int_of_rat: not an int";
 val lcm_rat = fn x => fn y => Rat.of_int (Integer.lcm (int_of_rat x) (int_of_rat y));
 

     n1 < n2 orelse n1 = n2 andalso lexorder m1 m2
     end;
 
 (* Arithmetic on canonical polynomials. *)
 
-fun grob_neg l = map (fn (c,m) => (minus_rat c,m)) l;
+fun grob_neg l = map (fn (c,m) => (Rat.neg c,m)) l;
 
 fun grob_add l1 l2 =
   case (l1,l2) of
     ([],l2) => l2
   | (l1,[]) => l1

 
 fun reduce1 cm (pol,hpol) =
   case pol of
     [] => error "reduce1"
   | cm1::cms => ((let val (c,m) = mdiv cm cm1 in
-                    (grob_cmul (minus_rat c,m) cms,
-                     Mmul((minus_rat c,m),hpol)) end)
+                    (grob_cmul (~ c, m) cms,
+                     Mmul ((~ c,m),hpol)) end)
                 handle  ERROR _ => error "reduce1");
 
 (* Try this for all polynomials in a basis.  *)
 fun tryfind f l =
     case l of

   | (_,([],h)) => ([],h)
   | ((cm1::ptl1,his1),(cm2::ptl2,his2)) =>
         (grob_sub (grob_cmul (mdiv cm cm1) ptl1)
                   (grob_cmul (mdiv cm cm2) ptl2),
          Add(Mmul(mdiv cm cm1,his1),
-             Mmul(mdiv (minus_rat(fst cm),snd cm) cm2,his2)));
+             Mmul(mdiv (~ (fst cm),snd cm) cm2,his2)));
 
 (* Make a polynomial monic.                                                  *)
 
 fun monic (pol,hist) =
   if null pol then (pol,hist) else

         Conv.fconv_rule ((Conv.arg_conv o Conv.arg_conv) (Conv.binop_conv ring_normalize_conv)) nth
        val th2 = funpow deg (idom_rule ctxt o HOLogic.conj_intr ctxt th1) neq_01
       in (vars,l,cert,th2)
       end)
     val cert_pos = map (fn (i,p) => (i,filter (fn (c,_) => c > @0) p)) cert
-    val cert_neg = map (fn (i,p) => (i,map (fn (c,m) => (minus_rat c,m))
+    val cert_neg = map (fn (i,p) => (i,map (fn (c,m) => (~ c,m))
                                             (filter (fn (c,_) => c < @0) p))) cert
     val  herts_pos = map (fn (i,p) => (i,holify_polynomial vars p)) cert_pos
     val  herts_neg = map (fn (i,p) => (i,holify_polynomial vars p)) cert_neg
     fun thm_fn pols =
         if null pols then Thm.reflexive(mk_const @0) else