diff -r 921a5be54132 -r 97b721666890 src/HOL/Multivariate_Analysis/normarith.ML
--- a/src/HOL/Multivariate_Analysis/normarith.ML	Wed Jun 01 15:01:43 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/normarith.ML	Wed Jun 01 15:10:27 2016 +0200
@@ -28,14 +28,14 @@
             find_normedterms (Thm.dest_arg1 t) (find_normedterms (Thm.dest_arg t) acc)
       | @{term "op * :: real => _"}$_$_ =>
             if not (is_ratconst (Thm.dest_arg1 t)) then acc else
-            augment_norm (dest_ratconst (Thm.dest_arg1 t) >= Rat.zero)
+            augment_norm (dest_ratconst (Thm.dest_arg1 t) >= @0)
                       (Thm.dest_arg t) acc
       | _ => augment_norm true t acc
 
  val cterm_lincomb_neg = FuncUtil.Ctermfunc.map (K Rat.neg)
  fun cterm_lincomb_cmul c t =
-    if c = Rat.zero 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 = Rat.zero) l r
+    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
  fun cterm_lincomb_sub l r = cterm_lincomb_add l (cterm_lincomb_neg r)
  fun cterm_lincomb_eq l r = FuncUtil.Ctermfunc.is_empty (cterm_lincomb_sub l r)
 
@@ -43,8 +43,8 @@
  val int_lincomb_neg = FuncUtil.Intfunc.map (K Rat.neg)
 *)
  fun int_lincomb_cmul c t =
-    if c = Rat.zero then FuncUtil.Intfunc.empty else FuncUtil.Intfunc.map (fn _ => fn x => x * c) t
- fun int_lincomb_add l r = FuncUtil.Intfunc.combine (curry op +) (fn x => x = Rat.zero) l r
+    if c = @0 then FuncUtil.Intfunc.empty else FuncUtil.Intfunc.map (fn _ => fn x => x * c) t
+ fun int_lincomb_add l r = FuncUtil.Intfunc.combine (curry op +) (fn x => x = @0) l r
 (*
  fun int_lincomb_sub l r = int_lincomb_add l (int_lincomb_neg r)
  fun int_lincomb_eq l r = FuncUtil.Intfunc.is_empty (int_lincomb_sub l r)
@@ -64,11 +64,11 @@
    let
      val b = ((snd o HOLogic.dest_number o term_of o Thm.dest_arg) t = 0
                handle TERM _=> false)
-   in if b then FuncUtil.Ctermfunc.onefunc (t,Rat.one)
+   in if b then FuncUtil.Ctermfunc.onefunc (t,@1)
       else FuncUtil.Ctermfunc.empty
    end
 *)
- | _ => FuncUtil.Ctermfunc.onefunc (t,Rat.one)
+ | _ => FuncUtil.Ctermfunc.onefunc (t,@1)
 
  fun vector_lincombs ts =
   fold_rev
@@ -84,7 +84,7 @@
 fun replacenegnorms cv t = case Thm.term_of t of
   @{term "op + :: real => _"}$_$_ => binop_conv (replacenegnorms cv) t
 | @{term "op * :: real => _"}$_$_ =>
-    if dest_ratconst (Thm.dest_arg1 t) < Rat.zero then arg_conv cv t else Thm.reflexive t
+    if dest_ratconst (Thm.dest_arg1 t) < @0 then arg_conv cv t else Thm.reflexive t
 | _ => Thm.reflexive t
 (*
 fun flip v eq =
@@ -97,10 +97,10 @@
                map (cons a) res @ res end
 fun evaluate env lin =
  FuncUtil.Intfunc.fold (fn (x,c) => fn s => s + c * (FuncUtil.Intfunc.apply env x))
-   lin Rat.zero
+   lin @0
 
 fun solve (vs,eqs) = case (vs,eqs) of
-  ([],[]) => SOME (FuncUtil.Intfunc.onefunc (0,Rat.one))
+  ([],[]) => SOME (FuncUtil.Intfunc.onefunc (0,@1))
  |(_,eq::oeqs) =>
    (case filter (member (op =) vs) (FuncUtil.Intfunc.dom eq) of (*FIXME use find_first here*)
      [] => NONE
@@ -127,9 +127,9 @@
  let
   fun vertex cmb = case solve(vs,cmb) of
     NONE => NONE
-   | SOME soln => SOME (map (fn v => FuncUtil.Intfunc.tryapplyd soln v Rat.zero) vs)
+   | SOME soln => SOME (map (fn v => FuncUtil.Intfunc.tryapplyd soln v @0) vs)
   val rawvs = map_filter vertex (combinations (length vs) eqs)
-  val unset = filter (forall (fn c => c >= Rat.zero)) rawvs
+  val unset = filter (forall (fn c => c >= @0)) rawvs
  in fold_rev (insert (eq_list op =)) unset []
  end
 
@@ -242,7 +242,7 @@
 (* FIXME
 | Const(@{const_name vec},_)$n =>
   let val n = Thm.dest_arg ct
-  in if is_ratconst n andalso not (dest_ratconst n =/ Rat.zero)
+  in if is_ratconst n andalso not (dest_ratconst n =/ @0)
      then Thm.reflexive ct else apply_pth1 ct
   end
 *)
@@ -288,7 +288,7 @@
       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
-     val inequalities = map (fn n => FuncUtil.Intfunc.onefunc (n,Rat.one)) nvs
+     val inequalities = map (fn n => FuncUtil.Intfunc.onefunc (n,@1)) nvs
      fun plausiblevertices f =
       let
        val flippedequations = map (fold_rev int_flip f) equations
@@ -296,8 +296,8 @@
        val rawverts = vertices nvs constraints
        fun check_solution v =
         let
-          val f = fold_rev FuncUtil.Intfunc.update (nvs ~~ v) (FuncUtil.Intfunc.onefunc (0, Rat.one))
-        in forall (fn e => evaluate f e = Rat.zero) flippedequations
+          val f = fold_rev FuncUtil.Intfunc.update (nvs ~~ v) (FuncUtil.Intfunc.onefunc (0, @1))
+        in forall (fn e => evaluate f e = @0) flippedequations
         end
        val goodverts = filter check_solution rawverts
        val signfixups = map (fn n => if member (op =) f n then ~1 else 1) nvs
@@ -308,7 +308,7 @@
     end
    fun compute_ineq v =
     let
-     val ths = map_filter (fn (v,t) => if v = Rat.zero then NONE
+     val ths = map_filter (fn (v,t) => if v = @0 then NONE
                                      else SOME(norm_cmul_rule v t))
                             (v ~~ nubs)
      fun end_itlist f xs = split_last xs |> uncurry (fold_rev f)