src/HOL/Tools/numeral_simprocs.ML

 
 (*Don't reduce fractions; sums must be proved by rule add_frac_eq.
   Fractions are reduced later by the cancel_numeral_factor simproc.*)
 fun add_frac ((p1, q1), (p2, q2)) = (p1 * q2 + p2 * q1, q1 * q2);
 
-val mk_divide = HOLogic.mk_binop @{const_name Rings.divide};
+val mk_divide = HOLogic.mk_binop @{const_name Fields.divide};
 
 (*Build term (p / q) * t*)
 fun mk_fcoeff ((p, q), t) =
   let val T = Term.fastype_of t
   in mk_times (mk_divide (mk_number T p, mk_number T q), t) end;
 
 (*Express t as a product of a fraction with other sorted terms*)
 fun dest_fcoeff sign (Const (@{const_name Groups.uminus}, _) $ t) = dest_fcoeff (~sign) t
-  | dest_fcoeff sign (Const (@{const_name Rings.divide}, _) $ t $ u) =
+  | dest_fcoeff sign (Const (@{const_name Fields.divide}, _) $ t $ u) =
     let val (p, t') = dest_coeff sign t
         val (q, u') = dest_coeff 1 u
     in (mk_frac (p, q), mk_divide (t', u')) end
   | dest_fcoeff sign t =
     let val (p, t') = dest_coeff sign t

 
 (*Version for fields*)
 structure DivideCancelNumeralFactor = CancelNumeralFactorFun
  (open CancelNumeralFactorCommon
   val prove_conv = Arith_Data.prove_conv
-  val mk_bal   = HOLogic.mk_binop @{const_name Rings.divide}
-  val dest_bal = HOLogic.dest_bin @{const_name Rings.divide} Term.dummyT
+  val mk_bal   = HOLogic.mk_binop @{const_name Fields.divide}
+  val dest_bal = HOLogic.dest_bin @{const_name Fields.divide} Term.dummyT
   val cancel = @{thm mult_divide_mult_cancel_left} RS trans
   val neg_exchanges = false
 )
 
 structure EqCancelNumeralFactor = CancelNumeralFactorFun

 
 (*Version for all fields, including unordered ones (type complex).*)
 structure DivideCancelFactor = ExtractCommonTermFun
  (open CancelFactorCommon
   val prove_conv = Arith_Data.prove_conv
-  val mk_bal   = HOLogic.mk_binop @{const_name Rings.divide}
-  val dest_bal = HOLogic.dest_bin @{const_name Rings.divide} Term.dummyT
+  val mk_bal   = HOLogic.mk_binop @{const_name Fields.divide}
+  val dest_bal = HOLogic.dest_bin @{const_name Fields.divide} Term.dummyT
   fun simp_conv _ _ = SOME @{thm mult_divide_mult_cancel_left_if}
 );
 
 val cancel_factors =
   map (Arith_Data.prep_simproc @{theory})

  fun proc2 phi ss ct =
   let
     val (l,r) = Thm.dest_binop ct
     val T = ctyp_of_term l
   in (case (term_of l, term_of r) of
-      (Const(@{const_name Rings.divide},_)$_$_, _) =>
+      (Const(@{const_name Fields.divide},_)$_$_, _) =>
         let val (x,y) = Thm.dest_binop l val z = r
             val _ = map (HOLogic.dest_number o term_of) [x,y,z]
             val ynz = prove_nz ss T y
         in SOME (Thm.implies_elim (instantiate' [SOME T] (map SOME [y,x,z]) add_frac_num) ynz)
         end
-     | (_, Const (@{const_name Rings.divide},_)$_$_) =>
+     | (_, Const (@{const_name Fields.divide},_)$_$_) =>
         let val (x,y) = Thm.dest_binop r val z = l
             val _ = map (HOLogic.dest_number o term_of) [x,y,z]
             val ynz = prove_nz ss T y
         in SOME (Thm.implies_elim (instantiate' [SOME T] (map SOME [y,z,x]) add_num_frac) ynz)
         end
      | _ => NONE)
   end
   handle CTERM _ => NONE | TERM _ => NONE | THM _ => NONE
 
- fun is_number (Const(@{const_name Rings.divide},_)$a$b) = is_number a andalso is_number b
+ fun is_number (Const(@{const_name Fields.divide},_)$a$b) = is_number a andalso is_number b
    | is_number t = can HOLogic.dest_number t
 
  val is_number = is_number o term_of
 
  fun proc3 phi ss ct =
   (case term_of ct of
-    Const(@{const_name Orderings.less},_)$(Const(@{const_name Rings.divide},_)$_$_)$_ =>
+    Const(@{const_name Orderings.less},_)$(Const(@{const_name Fields.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 Rings.divide},_)$_$_)$_ =>
+  | Const(@{const_name Orderings.less_eq},_)$(Const(@{const_name Fields.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_le_eq"}
       in SOME (mk_meta_eq th) end
-  | Const(@{const_name HOL.eq},_)$(Const(@{const_name Rings.divide},_)$_$_)$_ =>
+  | Const(@{const_name HOL.eq},_)$(Const(@{const_name Fields.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_eq_eq"}
       in SOME (mk_meta_eq th) end
-  | Const(@{const_name Orderings.less},_)$_$(Const(@{const_name Rings.divide},_)$_$_) =>
+  | Const(@{const_name Orderings.less},_)$_$(Const(@{const_name Fields.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 Rings.divide},_)$_$_) =>
+  | Const(@{const_name Orderings.less_eq},_)$_$(Const(@{const_name Fields.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 "le_divide_eq"}
       in SOME (mk_meta_eq th) end
-  | Const(@{const_name HOL.eq},_)$_$(Const(@{const_name Rings.divide},_)$_$_) =>
+  | Const(@{const_name HOL.eq},_)$_$(Const(@{const_name Fields.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 "eq_divide_eq"}