--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML Mon Feb 03 19:32:02 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML Mon Feb 03 19:32:02 2014 +0100
@@ -212,7 +212,7 @@
do_slice timeout 1 NONE Time.zeroTime
end
-fun run_smt_solver mode name (params as {debug, verbose, smt, preplay_timeout, ...})
+fun run_smt_solver mode name (params as {debug, verbose, smt_proofs, preplay_timeout, ...})
minimize_command ({state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) =
let
val thy = Proof.theory_of state
@@ -234,7 +234,7 @@
NONE =>
(Lazy.lazy (fn () =>
play_one_line_proof mode debug verbose preplay_timeout used_pairs state subgoal
- SMT_Method (bunch_of_proof_methods (smt <> SOME false) false liftingN)),
+ SMT_Method (bunch_of_proof_methods (smt_proofs <> SOME false) false liftingN)),
fn preplay =>
let
val one_line_params =