--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Aug 14 15:23:28 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Aug 14 15:26:45 2012 +0200
@@ -446,17 +446,17 @@
fun bunch_of_reconstructors needs_full_types lam_trans =
if needs_full_types then
+ [Metis (full_type_enc, lam_trans false),
+ Metis (really_full_type_enc, lam_trans false),
+ Metis (full_type_enc, lam_trans true),
+ Metis (really_full_type_enc, lam_trans true),
+ SMT]
+ else
[Metis (partial_type_enc, lam_trans false),
Metis (full_type_enc, lam_trans false),
Metis (no_typesN, lam_trans true),
Metis (really_full_type_enc, lam_trans true),
SMT]
- else
- [Metis (full_type_enc, lam_trans false),
- Metis (really_full_type_enc, lam_trans false),
- Metis (full_type_enc, lam_trans true),
- Metis (really_full_type_enc, lam_trans true),
- SMT]
fun extract_reconstructor ({type_enc, lam_trans, ...} : params)
(Metis (type_enc', lam_trans')) =