src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt2.ML
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 =>