src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML

 
 val reconstructor_names = [metisN, smtN]
 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
                     else SOME reconstr)
 

         let
           val used_facts = used_facts_in_atp_proof ctxt fact_names atp_proof
           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 () =>
               let
                 val used_ths =

       case outcome of
         NONE =>
         (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 =
                 (preplay, proof_banner mode name, used_facts,
                  choose_minimize_command minimize_command name preplay,