--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Mon Feb 03 15:33:18 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Mon Feb 03 16:53:58 2014 +0100
@@ -12,9 +12,9 @@
type stature = ATP_Problem_Generate.stature
type type_enc = ATP_Problem_Generate.type_enc
type fact = Sledgehammer_Fact.fact
- type proof_method = Sledgehammer_Reconstructor.proof_method
- type play_outcome = Sledgehammer_Reconstructor.play_outcome
- type minimize_command = Sledgehammer_Reconstructor.minimize_command
+ type proof_method = Sledgehammer_Proof_Methods.proof_method
+ type play_outcome = Sledgehammer_Proof_Methods.play_outcome
+ type minimize_command = Sledgehammer_Proof_Methods.minimize_command
datatype mode = Auto_Try | Try | Normal | MaSh | Auto_Minimize | Minimize
@@ -101,7 +101,7 @@
open ATP_Proof_Reconstruct
open Metis_Tactic
open Sledgehammer_Fact
-open Sledgehammer_Reconstructor
+open Sledgehammer_Proof_Methods
datatype mode = Auto_Try | Try | Normal | MaSh | Auto_Minimize | Minimize