--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Mon Aug 04 12:52:48 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Mon Aug 04 13:06:24 2014 +0200
@@ -362,9 +362,9 @@
val used_facts = sort_wrt fst (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 try0 (smt_proofs <> SOME false) needs_full_types
- (if atp_proof_prefers_lifting atp_proof then liftingN else hide_lamsN)
- |> `(hd o hd)
+ (Metis_Method (NONE, NONE),
+ bunches_of_proof_methods try0 (smt_proofs <> SOME false) needs_full_types
+ (if atp_proof_prefers_lifting atp_proof then liftingN else hide_lamsN))
in
(used_facts, preferred_methss,
fn preplay =>