src/HOL/Integ/int_factor_simprocs.ML

    [("field_eq_cancel_numeral_factor",
      ["(l::'a::{field,number_ring}) * m = n",
       "(l::'a::{field,number_ring}) = m * n"],
      FieldEqCancelNumeralFactor.proc),
     ("field_cancel_numeral_factor",
-     ["((l::'a::{field,number_ring}) * m) / n",
-      "(l::'a::{field,number_ring}) / (m * n)",
-      "((number_of v)::'a::{field,number_ring}) / (number_of w)"],
+     ["((l::'a::{division_by_zero,field,number_ring}) * m) / n",
+      "(l::'a::{division_by_zero,field,number_ring}) / (m * n)",
+      "((number_of v)::'a::{division_by_zero,field,number_ring}) / (number_of w)"],
      FieldDivCancelNumeralFactor.proc)]
 
 end;
 
 Addsimprocs ring_cancel_numeral_factors;

 fun cancel_simplify_meta_eq cancel_th th =
     Int_Numeral_Simprocs.simplify_meta_eq
         [mult_1, mult_1_right]
         (([th, cancel_th]) MRS trans);
 
+(*At present, long_mk_prod creates Numeral1, so this requires the axclass
+  number_ring*)
 structure CancelFactorCommon =
   struct
   val mk_sum            = long_mk_prod
   val dest_sum          = dest_prod
   val mk_coeff          = mk_coeff

   val mk_bal   = HOLogic.mk_binop "HOL.divide"
   val dest_bal = HOLogic.dest_bin "HOL.divide" Term.dummyT
   val simplify_meta_eq  = cancel_simplify_meta_eq mult_divide_cancel_eq_if
 );
 
+(*The number_ring class is necessary because the simprocs refer to the 
+  binary number 1.  FIXME: probably they could use 1 instead.*)
 val field_cancel_factor =
   map Bin_Simprocs.prep_simproc
    [("field_eq_cancel_factor",
-     ["(l::'a::field) * m = n", "(l::'a::field) = m * n"], 
+     ["(l::'a::{field,number_ring}) * m = n",
+      "(l::'a::{field,number_ring}) = m * n"], 
      FieldEqCancelFactor.proc),
     ("field_divide_cancel_factor",
-     ["((l::'a::field) * m) / n", "(l::'a::field) / (m * n)"],
+     ["((l::'a::{division_by_zero,field,number_ring}) * m) / n",
+      "(l::'a::{division_by_zero,field,number_ring}) / (m * n)"],
      FieldDivideCancelFactor.proc)];
 
 end;
 
 Addsimprocs int_cancel_factor;