--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Oct 18 11:59:45 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Oct 18 13:19:44 2012 +0200
@@ -11,9 +11,9 @@
type failure = ATP_Proof.failure
type stature = ATP_Problem_Generate.stature
type type_enc = ATP_Problem_Generate.type_enc
- type reconstructor = ATP_Proof_Reconstruct.reconstructor
- type play = ATP_Proof_Reconstruct.play
- type minimize_command = ATP_Proof_Reconstruct.minimize_command
+ type reconstructor = Sledgehammer_Reconstruct.reconstructor
+ type play = Sledgehammer_Reconstruct.play
+ type minimize_command = Sledgehammer_Reconstruct.minimize_command
datatype mode = Auto_Try | Try | Normal | MaSh | Auto_Minimize | Minimize