diff -r ce37d8f48a9f -r d87465cbfc9e src/HOL/Int.thy
--- a/src/HOL/Int.thy	Thu May 07 16:22:35 2009 +0200
+++ b/src/HOL/Int.thy	Fri May 08 08:00:11 2009 +0200
@@ -15,6 +15,9 @@
   "~~/src/Provers/Arith/assoc_fold.ML"
   "~~/src/Provers/Arith/cancel_numerals.ML"
   "~~/src/Provers/Arith/combine_numerals.ML"
+  "~~/src/Provers/Arith/cancel_numeral_factor.ML"
+  "~~/src/Provers/Arith/extract_common_term.ML"
+  ("Tools/int_factor_simprocs.ML")
   ("Tools/int_arith.ML")
 begin
 
@@ -1517,10 +1520,11 @@
 
 use "Tools/int_arith.ML"
 declaration {* K Int_Arith.setup *}
+use "Tools/int_factor_simprocs.ML"
 
 setup {*
   ReorientProc.add
-    (fn Const(@{const_name number_of}, _) $ _ => true | _ => false)
+    (fn Const (@{const_name number_of}, _) $ _ => true | _ => false)
 *}
 
 simproc_setup reorient_numeral ("number_of w = x") = ReorientProc.proc