src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
changeset 47148 0b8b73b49848
parent 47129 e2e52c7d25c9
child 47168 cac402c486b0
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Mon Jan 23 17:40:31 2012 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Mon Jan 23 17:40:32 2012 +0100
     1.3 @@ -8,7 +8,7 @@
     1.4  
     1.5  signature SLEDGEHAMMER_RUN =
     1.6  sig
     1.7 -  type minimize_command = ATP_Reconstruct.minimize_command
     1.8 +  type minimize_command = ATP_Proof_Reconstruct.minimize_command
     1.9    type relevance_override = Sledgehammer_Filter.relevance_override
    1.10    type mode = Sledgehammer_Provers.mode
    1.11    type params = Sledgehammer_Provers.params
    1.12 @@ -31,8 +31,8 @@
    1.13  struct
    1.14  
    1.15  open ATP_Util
    1.16 -open ATP_Translate
    1.17 -open ATP_Reconstruct
    1.18 +open ATP_Problem_Generate
    1.19 +open ATP_Proof_Reconstruct
    1.20  open Sledgehammer_Util
    1.21  open Sledgehammer_Filter
    1.22  open Sledgehammer_Provers