Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML
changeset 57742 1977a884fef7
parent 57739 b6af899a78ac
child 57750 670cbec816b9 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Fri Aug 01 14:43:57 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Fri Aug 01 14:43:57 2014 +0200
@@ -360,7 +360,7 @@
           val used_facts = used_facts_in_atp_proof ctxt (map fst used_from) atp_proof
           val needs_full_types = is_typed_helper_used_in_atp_proof atp_proof
           val preferred_methss =
-            bunches_of_proof_methods (smt_proofs <> SOME false) needs_full_types
+            bunches_of_proof_methods try0 (smt_proofs <> SOME false) needs_full_types
               (if atp_proof_prefers_lifting atp_proof then liftingN else hide_lamsN)
             |> `(hd o hd)
         in
isabelle