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 Algebras.divide};
+val mk_divide = HOLogic.mk_binop @{const_name Rings.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 Algebras.uminus}, _) $ t) = dest_fcoeff (~sign) t
-  | dest_fcoeff sign (Const (@{const_name Algebras.divide}, _) $ t $ u) =
+  | dest_fcoeff sign (Const (@{const_name Rings.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 Algebras.divide}
-  val dest_bal = HOLogic.dest_bin @{const_name Algebras.divide} Term.dummyT
+  val mk_bal   = HOLogic.mk_binop @{const_name Rings.divide}
+  val dest_bal = HOLogic.dest_bin @{const_name Rings.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 Algebras.divide}
-  val dest_bal = HOLogic.dest_bin @{const_name Algebras.divide} Term.dummyT
+  val mk_bal   = HOLogic.mk_binop @{const_name Rings.divide}
+  val dest_bal = HOLogic.dest_bin @{const_name Rings.divide} Term.dummyT
   fun simp_conv _ _ = SOME @{thm mult_divide_mult_cancel_left_if}
 );
 
 val cancel_factors =
   map (Arith_Data.prep_simproc @{theory})