--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML Mon Feb 03 23:20:12 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML Mon Feb 03 23:38:33 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_proofs, preplay_timeout, ...})
+fun run_smt_solver mode name (params as {verbose, smt_proofs, preplay_timeout, ...})
minimize_command ({state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) =
let
val thy = Proof.theory_of state
@@ -233,8 +233,8 @@
(case outcome of
NONE =>
(Lazy.lazy (fn () =>
- play_one_line_proof mode debug verbose preplay_timeout used_pairs state subgoal
- SMT_Method (bunch_of_proof_methods (smt_proofs <> SOME false) false liftingN)),
+ play_one_line_proof mode verbose preplay_timeout used_pairs state subgoal SMT_Method
+ (bunch_of_proof_methods (smt_proofs <> SOME false) false liftingN)),
fn preplay =>
let
val one_line_params =