diff -r d72ca5742f80 -r c0eafbd55de3 src/HOL/Numeral_Simprocs.thy
--- a/src/HOL/Numeral_Simprocs.thy	Wed Aug 22 22:47:16 2012 +0200
+++ b/src/HOL/Numeral_Simprocs.thy	Wed Aug 22 22:55:41 2012 +0200
@@ -4,16 +4,14 @@
 
 theory Numeral_Simprocs
 imports Divides
-uses
-  "~~/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/numeral_simprocs.ML")
-  ("Tools/nat_numeral_simprocs.ML")
 begin
 
+ML_file "~~/src/Provers/Arith/assoc_fold.ML"
+ML_file "~~/src/Provers/Arith/cancel_numerals.ML"
+ML_file "~~/src/Provers/Arith/combine_numerals.ML"
+ML_file "~~/src/Provers/Arith/cancel_numeral_factor.ML"
+ML_file "~~/src/Provers/Arith/extract_common_term.ML"
+
 lemmas semiring_norm =
   Let_def arith_simps nat_arith rel_simps
   if_False if_True
@@ -100,7 +98,7 @@
      "(k*m) div (k*n) = (if k = (0::nat) then 0 else m div n)"
 by (simp add: nat_mult_div_cancel1)
 
-use "Tools/numeral_simprocs.ML"
+ML_file "Tools/numeral_simprocs.ML"
 
 simproc_setup semiring_assoc_fold
   ("(a::'a::comm_semiring_1_cancel) * b") =
@@ -210,7 +208,7 @@
   |"(l::'a::field_inverse_zero) / (m * n)") =
   {* fn phi => Numeral_Simprocs.divide_cancel_factor *}
 
-use "Tools/nat_numeral_simprocs.ML"
+ML_file "Tools/nat_numeral_simprocs.ML"
 
 simproc_setup nat_combine_numerals
   ("(i::nat) + j" | "Suc (i + j)") =