# HG changeset patch
# User wenzelm
# Date 1362048023 -3600
# Node ID 30b014246e2150122a9b8cfed905ed40f92a5490
# Parent  ec7f10155389b054d0a6eced973985b1bed1ed23
proper place for cancel_div_mod.ML (see also ee729dbd1b7f and ec7f10155389);

diff -r ec7f10155389 -r 30b014246e21 src/HOL/Divides.thy
--- 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
 (
diff -r ec7f10155389 -r 30b014246e21 src/HOL/Nat_Transfer.thy
--- 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