--- a/src/HOL/int_factor_simprocs.ML Fri Jun 15 19:19:23 2007 +0200
+++ b/src/HOL/int_factor_simprocs.ML Sat Jun 16 15:01:54 2007 +0200
@@ -280,15 +280,15 @@
val cancel_factors =
map Int_Numeral_Base_Simprocs.prep_simproc
[("ring_eq_cancel_factor",
- ["(l::'a::{idom,number_ring}) * m = n",
- "(l::'a::{idom,number_ring}) = m * n"],
+ ["(l::'a::{idom}) * m = n",
+ "(l::'a::{idom}) = m * n"],
K EqCancelFactor.proc),
("int_div_cancel_factor",
["((l::int) * m) div n", "(l::int) div (m * n)"],
K IntDivCancelFactor.proc),
("divide_cancel_factor",
- ["((l::'a::{division_by_zero,field,number_ring}) * m) / n",
- "(l::'a::{division_by_zero,field,number_ring}) / (m * n)"],
+ ["((l::'a::{division_by_zero,field}) * m) / n",
+ "(l::'a::{division_by_zero,field}) / (m * n)"],
K DivideCancelFactor.proc)];
end;