diff -r 64b9806e160b -r 851c74f1bb69 src/HOL/Arith_Tools.thy
--- a/src/HOL/Arith_Tools.thy	Fri Jul 20 14:28:05 2007 +0200
+++ b/src/HOL/Arith_Tools.thy	Fri Jul 20 14:28:25 2007 +0200
@@ -480,14 +480,14 @@
 
  fun proc3 phi ss ct =
   (case term_of ct of
-    Const(@{const_name "Orderings.less"},_)$(Const(@{const_name "HOL.divide"},_)$_$_)$_ =>
+    Const(@{const_name HOL.less},_)$(Const(@{const_name "HOL.divide"},_)$_$_)$_ =>
       let
         val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
         val _ = map is_number [a,b,c]
         val T = ctyp_of_term c
         val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_less_eq"}
       in SOME (mk_meta_eq th) end
-  | Const(@{const_name "Orderings.less_eq"},_)$(Const(@{const_name "HOL.divide"},_)$_$_)$_ =>
+  | Const(@{const_name HOL.less_eq},_)$(Const(@{const_name "HOL.divide"},_)$_$_)$_ =>
       let
         val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
         val _ = map is_number [a,b,c]
@@ -501,14 +501,14 @@
         val T = ctyp_of_term c
         val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_eq_eq"}
       in SOME (mk_meta_eq th) end
-  | Const(@{const_name "Orderings.less"},_)$_$(Const(@{const_name "HOL.divide"},_)$_$_) =>
+  | Const(@{const_name HOL.less},_)$_$(Const(@{const_name "HOL.divide"},_)$_$_) =>
     let
       val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
         val _ = map is_number [a,b,c]
         val T = ctyp_of_term c
         val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "less_divide_eq"}
       in SOME (mk_meta_eq th) end
-  | Const(@{const_name "Orderings.less_eq"},_)$_$(Const(@{const_name "HOL.divide"},_)$_$_) =>
+  | Const(@{const_name HOL.less_eq},_)$_$(Const(@{const_name "HOL.divide"},_)$_$_) =>
     let
       val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
         val _ = map is_number [a,b,c]
@@ -745,7 +745,7 @@
 fun xnormalize_conv ctxt [] ct = reflexive ct
 | xnormalize_conv ctxt (vs as (x::_)) ct =
    case term_of ct of
-   Const(@{const_name "Orderings.less"},_)$_$Const(@{const_name "HOL.zero"},_) =>
+   Const(@{const_name HOL.less},_)$_$Const(@{const_name "HOL.zero"},_) =>
     (case whatis x (Thm.dest_arg1 ct) of
     ("c*x+t",[c,t]) =>
        let
@@ -788,7 +788,7 @@
     | _ => reflexive ct)
 
 
-|  Const(@{const_name "Orderings.less_eq"},_)$_$Const(@{const_name "HOL.zero"},_) =>
+|  Const(@{const_name HOL.less_eq},_)$_$Const(@{const_name "HOL.zero"},_) =>
    (case whatis x (Thm.dest_arg1 ct) of
     ("c*x+t",[c,t]) =>
        let
@@ -877,7 +877,7 @@
   val eq_iff_diff_eq_0 = mk_meta_eq @{thm "eq_iff_diff_eq_0"}
 in
 fun field_isolate_conv phi ctxt vs ct = case term_of ct of
-  Const(@{const_name "Orderings.less"},_)$a$b =>
+  Const(@{const_name HOL.less},_)$a$b =>
    let val (ca,cb) = Thm.dest_binop ct
        val T = ctyp_of_term ca
        val th = instantiate' [SOME T] [SOME ca, SOME cb] less_iff_diff_less_0
@@ -886,7 +886,7 @@
               (Normalizer.semiring_normalize_ord_conv @{context} (earlier vs)))) th
        val rth = transitive nth (xnormalize_conv ctxt vs (Thm.rhs_of nth))
    in rth end
-| Const(@{const_name "Orderings.less_eq"},_)$a$b =>
+| Const(@{const_name HOL.less_eq},_)$a$b =>
    let val (ca,cb) = Thm.dest_binop ct
        val T = ctyp_of_term ca
        val th = instantiate' [SOME T] [SOME ca, SOME cb] le_iff_diff_le_0
@@ -917,11 +917,11 @@
                             else Ferrante_Rackoff_Data.Nox
    | @{term "Not"}$(Const("op =", _)$y$z) => if term_of x aconv y then Ferrante_Rackoff_Data.NEq
                             else Ferrante_Rackoff_Data.Nox
-   | Const(@{const_name "Orderings.less"},_)$y$z =>
+   | Const(@{const_name HOL.less},_)$y$z =>
        if term_of x aconv y then Ferrante_Rackoff_Data.Lt
         else if term_of x aconv z then Ferrante_Rackoff_Data.Gt
         else Ferrante_Rackoff_Data.Nox
-   | Const (@{const_name "Orderings.less_eq"},_)$y$z =>
+   | Const (@{const_name HOL.less_eq},_)$y$z =>
          if term_of x aconv y then Ferrante_Rackoff_Data.Le
          else if term_of x aconv z then Ferrante_Rackoff_Data.Ge
          else Ferrante_Rackoff_Data.Nox