more adhoc overloading;
eliminated pointless Rat.eq: this is an equality type;
tuned;

--- a/NEWS	Wed Jun 01 17:46:12 2016 +0200
+++ b/NEWS	Wed Jun 01 19:23:18 2016 +0200
@@ -348,7 +348,7 @@
 *** ML ***
 
 * Ad-hoc overloading for standard operations on type Rat.rat: + - * / =
-< <= > >= <>. INCOMPATIBILITY, need to use + instead of +/ etc.
+< <= > >= <> ~ abs. INCOMPATIBILITY, need to use + instead of +/ etc.
 
 * The ML function "ML" provides easy access to run-time compilation.
 This is particularly useful for conditional compilation, without

--- a/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Wed Jun 01 17:46:12 2016 +0200
+++ b/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Wed Jun 01 19:23:18 2016 +0200
@@ -41,16 +41,12 @@
 
 fun round_rat r =
   let
-    val (a,b) = Rat.dest (Rat.abs r)
+    val (a,b) = Rat.dest (abs r)
     val d = a div b
-    val s = if r < @0 then (Rat.neg o Rat.of_int) else Rat.of_int
+    val s = if r < @0 then ~ o Rat.of_int else Rat.of_int
     val x2 = 2 * (a - (b * d))
   in s (if x2 >= b then d + 1 else d) end
 
-val abs_rat = Rat.abs;
-val pow2 = rat_pow @2;
-val pow10 = rat_pow @10;
-
 
 val trace = Attrib.setup_config_bool @{binding sos_trace} (K false);
 val debug = Attrib.setup_config_bool @{binding sos_debug} (K false);
@@ -74,8 +70,8 @@
 local
 
 fun normalize y =
-  if abs_rat y < @1/10 then normalize (@10 * y) - 1
-  else if abs_rat y >= @1 then normalize (y / @10) + 1
+  if abs y < @1/10 then normalize (@10 * y) - 1
+  else if abs y >= @1 then normalize (y / @10) + 1
   else 0
 
 in
@@ -84,10 +80,10 @@
   if x = @0 then "0.0"
   else
     let
-      val y = Rat.abs x
+      val y = abs x
       val e = normalize y
-      val z = pow10(~ e) * y + @1
-      val k = int_of_rat (round_rat(pow10 d * z))
+      val z = rat_pow @10 (~ e) * y + @1
+      val k = int_of_rat (round_rat (rat_pow @10 d * z))
     in
       (if x < @0 then "-0." else "0.") ^
       implode (tl (raw_explode(string_of_int k))) ^
@@ -182,7 +178,7 @@
   if c = @0 then poly_0
   else FuncUtil.Monomialfunc.map (fn _ => fn x => c * x) p;
 
-fun poly_neg p = FuncUtil.Monomialfunc.map (K Rat.neg) p;
+fun poly_neg p = FuncUtil.Monomialfunc.map (K ~) p;
 
 
 fun poly_add p1 p2 =
@@ -319,7 +315,7 @@
 val numeral = Scan.one isnum
 val decimalint = Scan.repeat1 numeral >> (rat_of_string o implode)
 val decimalfrac = Scan.repeat1 numeral
-  >> (fn s => rat_of_string(implode s) / pow10 (length s))
+  >> (fn s => rat_of_string(implode s) / rat_pow @10 (length s))
 val decimalsig =
   decimalint -- Scan.option (Scan.$$ "." |-- decimalfrac)
   >> (fn (h,NONE) => h | (h,SOME x) => h + x)
@@ -333,7 +329,7 @@
 val exponent = ($$ "e" || $$ "E") |-- signed decimalint;
 
 val decimal = signed decimalsig -- (emptyin @0|| exponent)
-  >> (fn (h, x) => h * pow10 (int_of_rat x));
+  >> (fn (h, x) => h * rat_pow @10 (int_of_rat x));
 
 fun mkparser p s =
   let val (x,rst) = p (raw_explode s)
@@ -359,7 +355,7 @@
   fun common_denominator fld amat acc =
     fld (fn (_,c) => fn a => lcm_rat (denominator_rat c) a) amat acc
   fun maximal_element fld amat acc =
-    fld (fn (_,c) => fn maxa => max_rat maxa (abs_rat c)) amat acc
+    fld (fn (_,c) => fn maxa => max_rat maxa (abs c)) amat acc
   fun float_of_rat x =
     let val (a,b) = Rat.dest x
     in Real.fromInt a / Real.fromInt b end;
@@ -374,8 +370,8 @@
     val obj' = vector_cmul cd2 obj
     val max1 = fold_rev (maximal_element Inttriplefunc.fold) mats' @0
     val max2 = maximal_element FuncUtil.Intfunc.fold (snd obj') @0
-    val scal1 = pow2 (20 - int_of_float(Math.ln (float_of_rat max1) / Math.ln 2.0))
-    val scal2 = pow2 (20 - int_of_float(Math.ln (float_of_rat max2) / Math.ln 2.0))
+    val scal1 = rat_pow @2 (20 - int_of_float(Math.ln (float_of_rat max1) / Math.ln 2.0))
+    val scal2 = rat_pow @2 (20 - int_of_float(Math.ln (float_of_rat max2) / Math.ln 2.0))
     val mats'' = map (Inttriplefunc.map (fn _ => fn x => x * scal1)) mats'
     val obj'' = vector_cmul scal2 obj'
   in solver obj'' mats'' end
@@ -438,7 +434,7 @@
               fun elim e =
                 let val b = Inttriplefunc.tryapplyd e v @0 in
                   if b = @0 then e
-                  else tri_equation_add e (tri_equation_cmul (Rat.neg b / a) eq)
+                  else tri_equation_add e (tri_equation_cmul (~ b / a) eq)
                 end
             in
               eliminate (Inttriplefunc.update(v, eq') (Inttriplefunc.map (K elim) dun))
@@ -559,7 +555,7 @@
 
 fun epoly_of_poly p =
   FuncUtil.Monomialfunc.fold (fn (m, c) => fn a =>
-      FuncUtil.Monomialfunc.update (m, Inttriplefunc.onefunc ((0, 0, 0), Rat.neg c)) a)
+      FuncUtil.Monomialfunc.update (m, Inttriplefunc.onefunc ((0, 0, 0), ~ c)) a)
     p FuncUtil.Monomialfunc.empty;
 
 (* String for block diagonal matrix numbered k.                              *)
@@ -725,7 +721,7 @@
       in (vec, map diag allmats) end
     val (vec, ratdias) =
       if null pvs then find_rounding @1
-      else tryfind find_rounding (map Rat.of_int (1 upto 31) @ map pow2 (5 upto 66))
+      else tryfind find_rounding (map Rat.of_int (1 upto 31) @ map (rat_pow @2) (5 upto 66))
     val newassigs =
       fold_rev (fn k => Inttriplefunc.update (nth pvs (k - 1), int_element vec k))
         (1 upto dim vec) (Inttriplefunc.onefunc ((0, 0, 0), Rat.of_int ~1))

--- a/src/HOL/Library/positivstellensatz.ML	Wed Jun 01 17:46:12 2016 +0200
+++ b/src/HOL/Library/positivstellensatz.ML	Wed Jun 01 19:23:18 2016 +0200
@@ -615,10 +615,10 @@
              in
                if c1 * c2 >= @0 then acc else
                let
-                 val e1' = linear_cmul (Rat.abs c2) e1
-                 val e2' = linear_cmul (Rat.abs c1) e2
-                 val p1' = Product(Rational_lt(Rat.abs c2),p1)
-                 val p2' = Product(Rational_lt(Rat.abs c1),p2)
+                 val e1' = linear_cmul (abs c2) e1
+                 val e2' = linear_cmul (abs c1) e2
+                 val p1' = Product(Rational_lt (abs c2), p1)
+                 val p2' = Product(Rational_lt (abs c1), p2)
                in (linear_add e1' e2',Sum(p1',p2'))::acc
                end
              end
@@ -653,11 +653,11 @@
              let val d = FuncUtil.Ctermfunc.tryapplyd t x @0 in
                if d = @0 then inp else
                let
-                 val k = (Rat.neg d) * Rat.abs c / c
+                 val k = ~ d * abs c / c
                  val e' = linear_cmul k e
-                 val t' = linear_cmul (Rat.abs c) t
+                 val t' = linear_cmul (abs c) t
                  val p' = Eqmul(FuncUtil.Monomialfunc.onefunc (FuncUtil.Ctermfunc.empty, k),p)
-                 val q' = Product(Rational_lt(Rat.abs c),q)
+                 val q' = Product(Rational_lt (abs c), q)
                in (linear_add e' t',Sum(p',q'))
                end
              end

--- a/src/HOL/Multivariate_Analysis/normarith.ML	Wed Jun 01 17:46:12 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/normarith.ML	Wed Jun 01 19:23:18 2016 +0200
@@ -32,7 +32,7 @@
                       (Thm.dest_arg t) acc
       | _ => augment_norm true t acc
 
- val cterm_lincomb_neg = FuncUtil.Ctermfunc.map (K Rat.neg)
+ val cterm_lincomb_neg = FuncUtil.Ctermfunc.map (K ~)
  fun cterm_lincomb_cmul c t =
     if c = @0 then FuncUtil.Ctermfunc.empty else FuncUtil.Ctermfunc.map (fn _ => fn x => x * c) t
  fun cterm_lincomb_add l r = FuncUtil.Ctermfunc.combine (curry op +) (fn x => x = @0) l r
@@ -40,7 +40,7 @@
  fun cterm_lincomb_eq l r = FuncUtil.Ctermfunc.is_empty (cterm_lincomb_sub l r)
 
 (*
- val int_lincomb_neg = FuncUtil.Intfunc.map (K Rat.neg)
+ val int_lincomb_neg = FuncUtil.Intfunc.map (K ~)
 *)
  fun int_lincomb_cmul c t =
     if c = @0 then FuncUtil.Intfunc.empty else FuncUtil.Intfunc.map (fn _ => fn x => x * c) t
@@ -89,7 +89,7 @@
 (*
 fun flip v eq =
   if FuncUtil.Ctermfunc.defined eq v
-  then FuncUtil.Ctermfunc.update (v, Rat.neg (FuncUtil.Ctermfunc.apply eq v)) eq else eq
+  then FuncUtil.Ctermfunc.update (v, ~ (FuncUtil.Ctermfunc.apply eq v)) eq else eq
 *)
 fun allsubsets s = case s of
   [] => [[]]
@@ -109,7 +109,7 @@
        then
         let
          val c = FuncUtil.Intfunc.apply eq v
-         val vdef = int_lincomb_cmul (Rat.neg (Rat.inv c)) eq
+         val vdef = int_lincomb_cmul (~ (Rat.inv c)) eq
          fun eliminate eqn = if not (FuncUtil.Intfunc.defined eqn v) then eqn
                              else int_lincomb_add (int_lincomb_cmul (FuncUtil.Intfunc.apply eqn v) vdef) eqn
         in (case solve (remove (op =) v vs, map eliminate oeqs) of
@@ -254,7 +254,7 @@
 
 fun int_flip v eq =
   if FuncUtil.Intfunc.defined eq v
-  then FuncUtil.Intfunc.update (v, Rat.neg (FuncUtil.Intfunc.apply eq v)) eq else eq;
+  then FuncUtil.Intfunc.update (v, ~ (FuncUtil.Intfunc.apply eq v)) eq else eq;
 
 local
  val pth_zero = @{thm norm_zero}
@@ -283,8 +283,10 @@
     let
      fun coefficients x =
       let
-       val inp = if FuncUtil.Ctermfunc.defined d x then FuncUtil.Intfunc.onefunc (0, Rat.neg(FuncUtil.Ctermfunc.apply d x))
-                      else FuncUtil.Intfunc.empty
+       val inp =
+        if FuncUtil.Ctermfunc.defined d x
+        then FuncUtil.Intfunc.onefunc (0, ~ (FuncUtil.Ctermfunc.apply d x))
+        else FuncUtil.Intfunc.empty
       in fold_rev (fn (f,v) => fn g => if FuncUtil.Ctermfunc.defined f x then FuncUtil.Intfunc.update (v, FuncUtil.Ctermfunc.apply f x) g else g) srccombs inp
       end
      val equations = map coefficients vvs

--- a/src/HOL/Tools/groebner.ML	Wed Jun 01 17:46:12 2016 +0200
+++ b/src/HOL/Tools/groebner.ML	Wed Jun 01 19:23:18 2016 +0200
@@ -32,7 +32,6 @@
   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";
@@ -70,7 +69,7 @@
 
 (* 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
@@ -131,8 +130,8 @@
   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.  *)
@@ -169,7 +168,7 @@
         (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.                                                  *)
 
@@ -711,7 +710,7 @@
       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

--- a/src/HOL/Tools/lin_arith.ML	Wed Jun 01 17:46:12 2016 +0200
+++ b/src/HOL/Tools/lin_arith.ML	Wed Jun 01 19:23:18 2016 +0200
@@ -171,7 +171,7 @@
         end
       else (SOME atom, m)
     (* terms that evaluate to numeric constants *)
-    | demult (Const (@{const_name Groups.uminus}, _) $ t, m) = demult (t, Rat.neg m)
+    | demult (Const (@{const_name Groups.uminus}, _) $ t, m) = demult (t, ~ m)
     | demult (Const (@{const_name Groups.zero}, _), _) = (NONE, @0)
     | demult (Const (@{const_name Groups.one}, _), m) = (NONE, m)
     (*Warning: in rare cases (neg_)numeral encloses a non-numeral,
@@ -200,9 +200,9 @@
   fun poly (Const (@{const_name Groups.plus}, _) $ s $ t,
         m : Rat.rat, pi : (term * Rat.rat) list * Rat.rat) = poly (s, m, poly (t, m, pi))
     | poly (all as Const (@{const_name Groups.minus}, T) $ s $ t, m, pi) =
-        if nT T then add_atom all m pi else poly (s, m, poly (t, Rat.neg m, pi))
+        if nT T then add_atom all m pi else poly (s, m, poly (t, ~ m, pi))
     | poly (all as Const (@{const_name Groups.uminus}, T) $ t, m, pi) =
-        if nT T then add_atom all m pi else poly (t, Rat.neg m, pi)
+        if nT T then add_atom all m pi else poly (t, ~ m, pi)
     | poly (Const (@{const_name Groups.zero}, _), _, pi) =
         pi
     | poly (Const (@{const_name Groups.one}, _), m, (p, i)) =

--- a/src/Pure/General/rat.ML	Wed Jun 01 17:46:12 2016 +0200
+++ b/src/Pure/General/rat.ML	Wed Jun 01 19:23:18 2016 +0200
@@ -13,7 +13,6 @@
   val dest: rat -> int * int
   val string_of_rat: rat -> string
   val signed_string_of_rat: rat -> string
-  val eq: rat * rat -> bool
   val ord: rat * rat -> order
   val le: rat -> rat -> bool
   val lt: rat -> rat -> bool
@@ -36,7 +35,7 @@
   let val m = PolyML.IntInf.lcm (q1, q2)
   in ((p1 * (m div q1), p2 * (m div q2)), m) end;
 
-fun make (p, 0) = raise Div
+fun make (_, 0) = raise Div
   | make (p, q) =
     let
       val m = PolyML.IntInf.gcd (p, q);
@@ -53,8 +52,6 @@
 fun signed_string_of_rat (Rat (p, 1)) = signed_string_of_int p
   | signed_string_of_rat (Rat (p, q)) = signed_string_of_int p ^ "/" ^ string_of_int q;
 
-fun eq (Rat (p1, q1), Rat (p2, q2)) = (p1 = p2 andalso q1 = q2);
-
 fun ord (Rat (p1, q1), Rat (p2, q2)) =
   (case (Integer.sign p1, Integer.sign p2) of
     (LESS, EQUAL) => LESS
@@ -66,12 +63,12 @@
   | (GREATER, EQUAL) => GREATER
   | _ => int_ord (fst (common (p1, q1) (p2, q2))));
 
-fun le a b = not (ord (a, b) = GREATER);
+fun le a b = ord (a, b) <> GREATER;
 fun lt a b = ord (a, b) = LESS;
 
 fun sign (Rat (p, _)) = Integer.sign p;
 
-fun abs (Rat (p, q)) = Rat (Int.abs p, q);
+fun abs (r as Rat (p, q)) = if p < 0 then Rat (~ p, q) else r;
 
 fun add (Rat (p1, q1)) (Rat (p2, q2)) =
   let val ((m1, m2), n) = common (p1, q1) (p2, q2)
@@ -100,11 +97,11 @@
 ML_system_overload (fn (a, b) => Rat.add a (Rat.neg b)) "-";
 ML_system_overload (uncurry Rat.mult) "*";
 ML_system_overload (fn (a, b) => Rat.mult a (Rat.inv b)) "/";
-ML_system_overload Rat.eq "=";
 ML_system_overload (uncurry Rat.lt) "<";
 ML_system_overload (uncurry Rat.le) "<=";
 ML_system_overload (fn (a, b) => Rat.lt b a) ">";
 ML_system_overload (fn (a, b) => Rat.le b a) ">=";
-ML_system_overload (not o Rat.eq) "<>";
+ML_system_overload Rat.neg "~";
+ML_system_overload Rat.abs "abs";
 
 ML_system_pp (fn _ => fn _ => fn x => Pretty.to_polyml (Pretty.str ("@" ^ Rat.string_of_rat x)));