diff -r d72ca5742f80 -r c0eafbd55de3 src/HOL/ATP.thy
--- a/src/HOL/ATP.thy	Wed Aug 22 22:47:16 2012 +0200
+++ b/src/HOL/ATP.thy	Wed Aug 22 22:55:41 2012 +0200
@@ -7,17 +7,15 @@
 
 theory ATP
 imports Meson
-uses "Tools/lambda_lifting.ML"
-     "Tools/monomorph.ML"
-     "Tools/ATP/atp_util.ML"
-     "Tools/ATP/atp_problem.ML"
-     "Tools/ATP/atp_proof.ML"
-     "Tools/ATP/atp_proof_redirect.ML"
-     ("Tools/ATP/atp_problem_generate.ML")
-     ("Tools/ATP/atp_proof_reconstruct.ML")
-     ("Tools/ATP/atp_systems.ML")
 begin
 
+ML_file "Tools/lambda_lifting.ML"
+ML_file "Tools/monomorph.ML"
+ML_file "Tools/ATP/atp_util.ML"
+ML_file "Tools/ATP/atp_problem.ML"
+ML_file "Tools/ATP/atp_proof.ML"
+ML_file "Tools/ATP/atp_proof_redirect.ML"
+
 subsection {* Higher-order reasoning helpers *}
 
 definition fFalse :: bool where [no_atp]:
@@ -132,9 +130,9 @@
 
 subsection {* Setup *}
 
-use "Tools/ATP/atp_problem_generate.ML"
-use "Tools/ATP/atp_proof_reconstruct.ML"
-use "Tools/ATP/atp_systems.ML"
+ML_file "Tools/ATP/atp_problem_generate.ML"
+ML_file "Tools/ATP/atp_proof_reconstruct.ML"
+ML_file "Tools/ATP/atp_systems.ML"
 
 setup ATP_Systems.setup