src/HOL/Decision_Procs/Dense_Linear_Order.thy

 | t => if t aconv term_of x then ("x",[]) else ("Nox",[]);
 
 fun xnormalize_conv ctxt [] ct = reflexive ct
 | xnormalize_conv ctxt (vs as (x::_)) ct =
    case term_of ct of
-   Const(@{const_name Algebras.less},_)$_$Const(@{const_name Algebras.zero},_) =>
+   Const(@{const_name Orderings.less},_)$_$Const(@{const_name Algebras.zero},_) =>
     (case whatis x (Thm.dest_arg1 ct) of
     ("c*x+t",[c,t]) =>
        let
         val cr = dest_frac c
         val clt = Thm.dest_fun2 ct

         val rth = th
       in rth end
     | _ => reflexive ct)
 
 
-|  Const(@{const_name Algebras.less_eq},_)$_$Const(@{const_name Algebras.zero},_) =>
+|  Const(@{const_name Orderings.less_eq},_)$_$Const(@{const_name Algebras.zero},_) =>
    (case whatis x (Thm.dest_arg1 ct) of
     ("c*x+t",[c,t]) =>
        let
         val T = ctyp_of_term x
         val cr = dest_frac c

   val less_iff_diff_less_0 = mk_meta_eq @{thm "less_iff_diff_less_0"}
   val le_iff_diff_le_0 = mk_meta_eq @{thm "le_iff_diff_le_0"}
   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 Algebras.less},_)$a$b =>
+  Const(@{const_name Orderings.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
        val nth = Conv.fconv_rule
          (Conv.arg_conv (Conv.arg1_conv
               (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 Algebras.less_eq},_)$a$b =>
+| Const(@{const_name Orderings.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
        val nth = Conv.fconv_rule
          (Conv.arg_conv (Conv.arg1_conv

    case term_of t of
      Const("op =", _)$y$z => if term_of x aconv y then Ferrante_Rackoff_Data.Eq
                             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 Algebras.less},_)$y$z =>
+   | Const(@{const_name Orderings.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 Algebras.less_eq},_)$y$z =>
+   | Const (@{const_name Orderings.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
    | _ => Ferrante_Rackoff_Data.Nox
  in h end;