--- a/src/HOL/ATP.thy Mon Jan 23 17:40:31 2012 +0100
+++ b/src/HOL/ATP.thy Mon Jan 23 17:40:32 2012 +0100
@@ -12,9 +12,9 @@
"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
@@ -49,8 +49,8 @@
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