--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML Thu May 22 03:29:35 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML Thu May 22 03:29:36 2014 +0200
@@ -238,7 +238,7 @@
(case outcome of
NONE =>
(Lazy.lazy (fn () =>
- play_one_line_proof mode debug verbose preplay_timeout used_named_facts state subgoal
+ play_one_line_proof mode verbose preplay_timeout used_named_facts state subgoal
SMT2_Method (bunch_of_proof_methods (smt_proofs <> SOME false) false liftingN)),
fn preplay =>
let