# HG changeset patch
# User blanchet
# Date 1321613232 -3600
# Node ID 1606122a2d0f547b7ea92725c57a15a4e3038e03
# Parent  22d6fb988306437fa6cb0d10659a714e5015bf3c
don't needlessly pass "lam_lifted" option to "metis" call for SMT proof

diff -r 22d6fb988306 -r 1606122a2d0f src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Fri Nov 18 11:47:12 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Fri Nov 18 11:47:12 2011 +0100
@@ -146,9 +146,9 @@
 val plain_metis = Metis (hd partial_type_encs, combinatorsN)
 
 fun bunch_of_reconstructors needs_full_types lam_trans =
-  [(false, Metis (hd partial_type_encs, lam_trans metis_default_lam_trans)),
-   (true, Metis (hd full_type_encs, lam_trans hide_lamsN)),
-   (false, Metis (no_type_enc, lam_trans hide_lamsN)),
+  [(false, Metis (hd partial_type_encs, lam_trans true)),
+   (true, Metis (hd full_type_encs, lam_trans false)),
+   (false, Metis (no_type_enc, lam_trans false)),
    (true, SMT)]
   |> map_filter (fn (full_types, reconstr) =>
                     if needs_full_types andalso not full_types then NONE
@@ -786,7 +786,9 @@
           val needs_full_types = is_typed_helper_used_in_proof atp_proof
           val reconstrs =
             bunch_of_reconstructors needs_full_types
-                                    (lam_trans_from_atp_proof atp_proof)
+                (lam_trans_from_atp_proof atp_proof
+                 o (fn plain =>
+                       if plain then metis_default_lam_trans else hide_lamsN))
         in
           (used_facts,
            fn () =>
@@ -977,7 +979,10 @@
         (fn () =>
             play_one_line_proof mode debug verbose preplay_timeout used_ths
                 state subgoal SMT
-                (bunch_of_reconstructors false (K lam_liftingN)),
+                (bunch_of_reconstructors false
+                     (fn plain =>
+                         if plain then metis_default_lam_trans
+                         else lam_liftingN)),
          fn preplay =>
             let
               val one_line_params =