# HG changeset patch
# User blanchet
# Date 1328288455 -3600
# Node ID 76ed3b7092fc642861d0e9723749698c57d2e437
# Parent  7736068b9f56edba69c711a77ef0a093bf00f7bf
try to pass fewer options to Metis

diff -r 7736068b9f56 -r 76ed3b7092fc src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Fri Feb 03 15:51:10 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Fri Feb 03 18:00:55 2012 +0100
@@ -399,10 +399,10 @@
   | _ => "Try this"
 
 fun bunch_of_reconstructors needs_full_types lam_trans =
-  [(false, Metis (partial_type_enc, lam_trans true)),
+  [(false, Metis (partial_type_enc, lam_trans false)),
    (true, Metis (full_type_enc, lam_trans false)),
-   (false, Metis (no_typesN, lam_trans false)),
-   (true, Metis (really_full_type_enc, lam_trans false)),
+   (false, Metis (no_typesN, lam_trans true)),
+   (true, Metis (really_full_type_enc, lam_trans true)),
    (true, SMT)]
   |> map_filter (fn (full_types, reconstr) =>
                     if needs_full_types andalso not full_types then NONE
@@ -798,8 +798,8 @@
           val reconstrs =
             bunch_of_reconstructors needs_full_types
                 (lam_trans_from_atp_proof atp_proof
-                 o (fn plain =>
-                       if plain then metis_default_lam_trans else hide_lamsN))
+                 o (fn desperate => if desperate then hide_lamsN
+                                    else metis_default_lam_trans))
         in
           (used_facts,
            fn () =>