--- a/src/HOL/Divides.thy Wed Feb 27 20:36:21 2013 +0100
+++ b/src/HOL/Divides.thy Thu Feb 28 11:40:23 2013 +0100
@@ -686,6 +686,8 @@
text {* Simproc for cancelling @{const div} and @{const mod} *}
+ML_file "~~/src/Provers/Arith/cancel_div_mod.ML"
+
ML {*
structure Cancel_Div_Mod_Nat = Cancel_Div_Mod
(
--- a/src/HOL/Nat_Transfer.thy Wed Feb 27 20:36:21 2013 +0100
+++ b/src/HOL/Nat_Transfer.thy Thu Feb 28 11:40:23 2013 +0100
@@ -420,8 +420,4 @@
return: transfer_int_nat_sum_prod transfer_int_nat_sum_prod2
cong: setsum_cong setprod_cong]
-
-(*belongs to Divides.thy, but slows down dependency discovery*)
-ML_file "~~/src/Provers/Arith/cancel_div_mod.ML"
-
end