1.1 --- a/src/HOL/ATP.thy	Mon Jan 23 17:40:31 2012 +0100
     1.2 +++ b/src/HOL/ATP.thy	Mon Jan 23 17:40:32 2012 +0100
     1.3 @@ -12,9 +12,9 @@
     1.4       "Tools/ATP/atp_util.ML"
     1.5       "Tools/ATP/atp_problem.ML"
     1.6       "Tools/ATP/atp_proof.ML"
     1.7 -     "Tools/ATP/atp_redirect.ML"
     1.8 -     ("Tools/ATP/atp_translate.ML")
     1.9 -     ("Tools/ATP/atp_reconstruct.ML")
    1.10 +     "Tools/ATP/atp_proof_redirect.ML"
    1.11 +     ("Tools/ATP/atp_problem_generate.ML")
    1.12 +     ("Tools/ATP/atp_proof_reconstruct.ML")
    1.13       ("Tools/ATP/atp_systems.ML")
    1.14  begin
    1.15  
    1.16 @@ -49,8 +49,8 @@
    1.17  
    1.18  subsection {* Setup *}
    1.19  
    1.20 -use "Tools/ATP/atp_translate.ML"
    1.21 -use "Tools/ATP/atp_reconstruct.ML"
    1.22 +use "Tools/ATP/atp_problem_generate.ML"
    1.23 +use "Tools/ATP/atp_proof_reconstruct.ML"
    1.24  use "Tools/ATP/atp_systems.ML"
    1.25  
    1.26  setup ATP_Systems.setup