diff -r 7bbbd9393ce0 -r ffa306239316 src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Mon Feb 03 15:33:18 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Mon Feb 03 16:53:58 2014 +0100
@@ -38,7 +38,7 @@
 open ATP_Problem_Generate
 open ATP_Proof_Reconstruct
 open Sledgehammer_Util
-open Sledgehammer_Reconstructor
+open Sledgehammer_Proof_Methods
 open Sledgehammer_Prover
 
 val smt_builtins = Attrib.setup_config_bool @{binding sledgehammer_smt_builtins} (K true)