src/HOL/Tools/numeral_simprocs.ML

      K CombineNumerals.proc);
 
 val field_combine_numerals =
   Arith_Data.prep_simproc @{theory}
     ("field_combine_numerals", 
-     ["(i::'a::{number_ring,field,division_ring_inverse_zero}) + j",
-      "(i::'a::{number_ring,field,division_ring_inverse_zero}) - j"], 
+     ["(i::'a::{field_inverse_zero, number_ring}) + j",
+      "(i::'a::{field_inverse_zero, number_ring}) - j"], 
      K FieldCombineNumerals.proc);
 
 (** Constant folding for multiplication in semirings **)
 
 (*We do not need folding for addition: combine_numerals does the same thing*)

     ("int_div_cancel_numeral_factors",
      ["((l::'a::{semiring_div,number_ring}) * m) div n",
       "(l::'a::{semiring_div,number_ring}) div (m * n)"],
      K DivCancelNumeralFactor.proc),
     ("divide_cancel_numeral_factor",
-     ["((l::'a::{division_ring_inverse_zero,field,number_ring}) * m) / n",
-      "(l::'a::{division_ring_inverse_zero,field,number_ring}) / (m * n)",
-      "((number_of v)::'a::{division_ring_inverse_zero,field,number_ring}) / (number_of w)"],
+     ["((l::'a::{field_inverse_zero,number_ring}) * m) / n",
+      "(l::'a::{field_inverse_zero,number_ring}) / (m * n)",
+      "((number_of v)::'a::{field_inverse_zero,number_ring}) / (number_of w)"],
      K DivideCancelNumeralFactor.proc)];
 
 val field_cancel_numeral_factors =
   map (Arith_Data.prep_simproc @{theory})
    [("field_eq_cancel_numeral_factor",
      ["(l::'a::{field,number_ring}) * m = n",
       "(l::'a::{field,number_ring}) = m * n"],
      K EqCancelNumeralFactor.proc),
     ("field_cancel_numeral_factor",
-     ["((l::'a::{division_ring_inverse_zero,field,number_ring}) * m) / n",
-      "(l::'a::{division_ring_inverse_zero,field,number_ring}) / (m * n)",
-      "((number_of v)::'a::{division_ring_inverse_zero,field,number_ring}) / (number_of w)"],
+     ["((l::'a::{field_inverse_zero,number_ring}) * m) / n",
+      "(l::'a::{field_inverse_zero,number_ring}) / (m * n)",
+      "((number_of v)::'a::{field_inverse_zero,number_ring}) / (number_of w)"],
      K DivideCancelNumeralFactor.proc)]
 
 
 (** Declarations for ExtractCommonTerm **)
 

      K ModCancelFactor.proc),
     ("dvd_cancel_factor",
      ["((l::'a::idom) * m) dvd n", "(l::'a::idom) dvd (m * n)"],
      K DvdCancelFactor.proc),
     ("divide_cancel_factor",
-     ["((l::'a::{division_ring_inverse_zero,field}) * m) / n",
-      "(l::'a::{division_ring_inverse_zero,field}) / (m * n)"],
+     ["((l::'a::field_inverse_zero) * m) / n",
+      "(l::'a::field_inverse_zero) / (m * n)"],
      K DivideCancelFactor.proc)];
 
 end;
 
 Addsimprocs Numeral_Simprocs.cancel_numerals;