changeset 57742 | 1977a884fef7 |
parent 57739 | b6af899a78ac |
child 57750 | 670cbec816b9 |
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML Fri Aug 01 14:43:57 2014 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML Fri Aug 01 14:43:57 2014 +0200 @@ -197,7 +197,7 @@ NONE => let val preferred_methss = - (SMT2_Method, bunches_of_proof_methods (smt_proofs <> SOME false) false liftingN) + (SMT2_Method, bunches_of_proof_methods try0 (smt_proofs <> SOME false) false liftingN) in (preferred_methss, fn preplay =>