try right bunch of methods
authorblanchet
Thu Feb 06 01:13:44 2014 +0100 (2014-02-06 ago)
changeset 553458a53ee72e595
parent 55344 a593712f6878
child 55346 d344d663658a
try right bunch of methods
src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Thu Feb 06 00:43:57 2014 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Thu Feb 06 01:13:44 2014 +0100
     1.3 @@ -187,15 +187,16 @@
     1.4    | _ => "Try this")
     1.5  
     1.6  fun bunch_of_proof_methods smt_proofs needs_full_types desperate_lam_trans =
     1.7 -  [Metis_Method (SOME full_type_enc, NONE)] @
     1.8    (if needs_full_types then
     1.9 -     [Metis_Method (SOME full_type_enc, NONE),
    1.10 +     [Metis_Method (SOME full_typesN, NONE),
    1.11        Metis_Method (SOME really_full_type_enc, NONE),
    1.12 -      Metis_Method (SOME full_type_enc, SOME desperate_lam_trans)]
    1.13 +      Metis_Method (SOME full_typesN, SOME desperate_lam_trans),
    1.14 +      Metis_Method (SOME really_full_type_enc, SOME desperate_lam_trans)]
    1.15     else
    1.16       [Metis_Method (NONE, NONE),
    1.17 -      Metis_Method (SOME no_typesN, SOME desperate_lam_trans)]) @
    1.18 -  [Metis_Method (SOME really_full_type_enc, SOME desperate_lam_trans)] @
    1.19 +      Metis_Method (SOME full_typesN, NONE),
    1.20 +      Metis_Method (SOME no_typesN, SOME desperate_lam_trans),
    1.21 +      Metis_Method (SOME really_full_type_enc, SOME desperate_lam_trans)]) @
    1.22    (if smt_proofs then [SMT_Method] else [])
    1.23  
    1.24  fun extract_proof_method ({type_enc, lam_trans, ...} : params)