--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Thu Feb 06 00:43:57 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Thu Feb 06 01:13:44 2014 +0100
@@ -187,15 +187,16 @@
| _ => "Try this")
fun bunch_of_proof_methods smt_proofs needs_full_types desperate_lam_trans =
- [Metis_Method (SOME full_type_enc, NONE)] @
(if needs_full_types then
- [Metis_Method (SOME full_type_enc, NONE),
+ [Metis_Method (SOME full_typesN, NONE),
Metis_Method (SOME really_full_type_enc, NONE),
- Metis_Method (SOME full_type_enc, SOME desperate_lam_trans)]
+ Metis_Method (SOME full_typesN, SOME desperate_lam_trans),
+ Metis_Method (SOME really_full_type_enc, SOME desperate_lam_trans)]
else
[Metis_Method (NONE, NONE),
- Metis_Method (SOME no_typesN, SOME desperate_lam_trans)]) @
- [Metis_Method (SOME really_full_type_enc, SOME desperate_lam_trans)] @
+ Metis_Method (SOME full_typesN, NONE),
+ Metis_Method (SOME no_typesN, SOME desperate_lam_trans),
+ Metis_Method (SOME really_full_type_enc, SOME desperate_lam_trans)]) @
(if smt_proofs then [SMT_Method] else [])
fun extract_proof_method ({type_enc, lam_trans, ...} : params)