src/HOL/ATP.thy

 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_redirect.ML"
-     ("Tools/ATP/atp_translate.ML")
-     ("Tools/ATP/atp_reconstruct.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
 
 subsection {* Higher-order reasoning helpers *}
 

 definition fEx :: "('a \<Rightarrow> bool) \<Rightarrow> bool" where [no_atp]:
 "fEx P \<longleftrightarrow> Ex P"
 
 subsection {* Setup *}
 
-use "Tools/ATP/atp_translate.ML"
-use "Tools/ATP/atp_reconstruct.ML"
+use "Tools/ATP/atp_problem_generate.ML"
+use "Tools/ATP/atp_proof_reconstruct.ML"
 use "Tools/ATP/atp_systems.ML"
 
 setup ATP_Systems.setup
 
 end