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