--- a/src/HOL/Divides.thy Wed Aug 25 18:19:04 2010 +0200
+++ b/src/HOL/Divides.thy Wed Aug 25 18:36:22 2010 +0200
@@ -700,7 +700,7 @@
in
-val cancel_div_mod_nat_proc = Simplifier.simproc @{theory}
+val cancel_div_mod_nat_proc = Simplifier.simproc_global @{theory}
"cancel_div_mod" ["(m::nat) + n"] (K CancelDivMod.proc);
val _ = Addsimprocs [cancel_div_mod_nat_proc];
@@ -1459,7 +1459,7 @@
in
-val cancel_div_mod_int_proc = Simplifier.simproc @{theory}
+val cancel_div_mod_int_proc = Simplifier.simproc_global @{theory}
"cancel_zdiv_zmod" ["(k::int) + l"] (K CancelDivMod.proc);
val _ = Addsimprocs [cancel_div_mod_int_proc];