src/HOL/Tools/Qelim/cooper.ML

    if term_of x aconv y then Lt (Thm.dest_arg ct)
    else if term_of x aconv z then Gt (Thm.dest_arg1 ct) else Nox
 | Const (@{const_name Algebras.less_eq}, _) $ y $ z =>
    if term_of x aconv y then Le (Thm.dest_arg ct)
    else if term_of x aconv z then Ge (Thm.dest_arg1 ct) else Nox
-| Const (@{const_name Ring_and_Field.dvd},_)$_$(Const(@{const_name Algebras.plus},_)$y$_) =>
+| Const (@{const_name Rings.dvd},_)$_$(Const(@{const_name Algebras.plus},_)$y$_) =>
    if term_of x aconv y then Dvd (Thm.dest_binop ct ||> Thm.dest_arg) else Nox
-| Const (@{const_name Not},_) $ (Const (@{const_name Ring_and_Field.dvd},_)$_$(Const(@{const_name Algebras.plus},_)$y$_)) =>
+| Const (@{const_name Not},_) $ (Const (@{const_name Rings.dvd},_)$_$(Const(@{const_name Algebras.plus},_)$y$_)) =>
    if term_of x aconv y then
    NDvd (Thm.dest_binop (Thm.dest_arg ct) ||> Thm.dest_arg) else Nox
 | _ => Nox)
   handle CTERM _ => Nox;
 

 fun lin (vs as x::_) (Const (@{const_name Not}, _) $ (Const (@{const_name Algebras.less}, T) $ s $ t)) =
     lin vs (Const (@{const_name Algebras.less_eq}, T) $ t $ s)
   | lin (vs as x::_) (Const (@{const_name Not},_) $ (Const(@{const_name Algebras.less_eq}, T) $ s $ t)) =
     lin vs (Const (@{const_name Algebras.less}, T) $ t $ s)
   | lin vs (Const (@{const_name Not},T)$t) = Const (@{const_name Not},T)$ (lin vs t)
-  | lin (vs as x::_) (Const(@{const_name Ring_and_Field.dvd},_)$d$t) =
-    HOLogic.mk_binrel @{const_name Ring_and_Field.dvd} (numeral1 abs d, lint vs t)
+  | lin (vs as x::_) (Const(@{const_name Rings.dvd},_)$d$t) =
+    HOLogic.mk_binrel @{const_name Rings.dvd} (numeral1 abs d, lint vs t)
   | lin (vs as x::_) ((b as Const("op =",_))$s$t) =
      (case lint vs (subC$t$s) of
       (t as a$(m$c$y)$r) =>
         if x <> y then b$zero$t
         else if dest_numeral c < 0 then b$(m$(numeral1 ~ c)$y)$r

 fun is_intrel (b$_$_) = is_intrel_type (fastype_of b)
   | is_intrel (@{term "Not"}$(b$_$_)) = is_intrel_type (fastype_of b)
   | is_intrel _ = false;
 
 fun linearize_conv ctxt vs ct = case term_of ct of
-  Const(@{const_name Ring_and_Field.dvd},_)$d$t =>
+  Const(@{const_name Rings.dvd},_)$d$t =>
   let
     val th = binop_conv (lint_conv ctxt vs) ct
     val (d',t') = Thm.dest_binop (Thm.rhs_of th)
     val (dt',tt') = (term_of d', term_of t')
   in if is_numeral dt' andalso is_numeral tt'

                                        (Thm.transitive dth (inst' [d'',t'] dvd_uminus'))
         else dth end
       | _ => dth
      end
   end
-| Const (@{const_name Not},_)$(Const(@{const_name Ring_and_Field.dvd},_)$_$_) => arg_conv (linearize_conv ctxt vs) ct
+| Const (@{const_name Not},_)$(Const(@{const_name Rings.dvd},_)$_$_) => arg_conv (linearize_conv ctxt vs) ct
 | t => if is_intrel t
       then (provelin ctxt ((HOLogic.eq_const bT)$t$(lin vs t) |> HOLogic.mk_Trueprop))
        RS eq_reflection
       else reflexive ct;
 

     then (ins (dest_numeral c) acc,dacc) else (acc,dacc)
   | Const(s,_)$_$(Const(@{const_name Algebras.times},_)$c$y) =>
     if x aconv y andalso member (op =)
        [@{const_name Algebras.less}, @{const_name Algebras.less_eq}] s
     then (ins (dest_numeral c) acc, dacc) else (acc,dacc)
-  | Const(@{const_name Ring_and_Field.dvd},_)$_$(Const(@{const_name Algebras.plus},_)$(Const(@{const_name Algebras.times},_)$c$y)$_) =>
+  | Const(@{const_name Rings.dvd},_)$_$(Const(@{const_name Algebras.plus},_)$(Const(@{const_name Algebras.times},_)$c$y)$_) =>
     if x aconv y then (acc,ins (dest_numeral c) dacc) else (acc,dacc)
   | Const("op &",_)$_$_ => h (h (acc,dacc) (Thm.dest_arg1 t)) (Thm.dest_arg t)
   | Const("op |",_)$_$_ => h (h (acc,dacc) (Thm.dest_arg1 t)) (Thm.dest_arg t)
   | Const (@{const_name Not},_)$_ => h (acc,dacc) (Thm.dest_arg t)
   | _ => (acc, dacc)

     then cv (l div dest_numeral c) t else Thm.reflexive t
   | Const(s,_)$_$(Const(@{const_name Algebras.times},_)$c$y) =>
     if x=y andalso member (op =)
       [@{const_name Algebras.less}, @{const_name Algebras.less_eq}] s
     then cv (l div dest_numeral c) t else Thm.reflexive t
-  | Const(@{const_name Ring_and_Field.dvd},_)$d$(r as (Const(@{const_name Algebras.plus},_)$(Const(@{const_name Algebras.times},_)$c$y)$_)) =>
+  | Const(@{const_name Rings.dvd},_)$d$(r as (Const(@{const_name Algebras.plus},_)$(Const(@{const_name Algebras.times},_)$c$y)$_)) =>
     if x=y then
       let
        val k = l div dest_numeral c
        val kt = HOLogic.mk_number iT k
        val th1 = inst' [Thm.dest_arg1 t, Thm.dest_arg t]

 fun qf_of_term ps vs t =  case t
  of Const("True",_) => T
   | Const("False",_) => F
   | Const(@{const_name Algebras.less},_)$t1$t2 => Lt (Sub (i_of_term vs t1,i_of_term vs t2))
   | Const(@{const_name Algebras.less_eq},_)$t1$t2 => Le (Sub(i_of_term vs t1,i_of_term vs t2))
-  | Const(@{const_name Ring_and_Field.dvd},_)$t1$t2 =>
+  | Const(@{const_name Rings.dvd},_)$t1$t2 =>
       (Dvd(HOLogic.dest_number t1 |> snd, i_of_term vs t2) handle _ => cooper "Reification: unsupported dvd")  (* FIXME avoid handle _ *)
   | @{term "op = :: int => _"}$t1$t2 => Eq (Sub (i_of_term vs t1,i_of_term vs t2))
   | @{term "op = :: bool => _ "}$t1$t2 => Iff(qf_of_term ps vs t1,qf_of_term ps vs t2)
   | Const("op &",_)$t1$t2 => And(qf_of_term ps vs t1,qf_of_term ps vs t2)
   | Const("op |",_)$t1$t2 => Or(qf_of_term ps vs t1,qf_of_term ps vs t2)