diff -r fbc60cd02ae2 -r a657683e902a src/HOL/IntDiv.thy
--- a/src/HOL/IntDiv.thy	Wed Feb 20 14:52:34 2008 +0100
+++ b/src/HOL/IntDiv.thy	Wed Feb 20 14:52:38 2008 +0100
@@ -274,13 +274,13 @@
   val prove_eq_sums =
     let
       val simps = @{thm diff_int_def} :: Int_Numeral_Simprocs.add_0s @ @{thms zadd_ac}
-    in NatArithUtils.prove_conv all_tac (NatArithUtils.simp_all_tac simps) end;
+    in ArithData.prove_conv all_tac (ArithData.simp_all_tac simps) end;
 end)
 
 in
 
-val cancel_zdiv_zmod_proc = NatArithUtils.prep_simproc
-  ("cancel_zdiv_zmod", ["(m::int) + n"], K CancelDivMod.proc)
+val cancel_zdiv_zmod_proc = Simplifier.simproc @{theory}
+  "cancel_zdiv_zmod" ["(m::int) + n"] (K CancelDivMod.proc)
 
 end;