changeset 55287 | ffa306239316 |
parent 55285 | e88ad20035f4 |
child 55288 | 1a4358d14ce2 |
--- 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)