src/HOL/Tools/Metis/metis_tactic.ML

 (* Main function to start Metis proof and reconstruction *)
 fun FOL_SOLVE (type_enc :: fallback_type_encs) lam_trans ctxt cls ths0 =
   let val thy = Proof_Context.theory_of ctxt
       val new_skolemizer =
         Config.get ctxt new_skolemizer orelse null (Meson.choice_theorems thy)
-      val do_lams = lam_trans = lam_liftingN ? introduce_lam_wrappers ctxt
+      val do_lams =
+        (lam_trans = liftingN orelse lam_trans = lam_liftingN)
+        ? introduce_lam_wrappers ctxt
       val th_cls_pairs =
         map2 (fn j => fn th =>
                 (Thm.get_name_hint th,
                  th |> Drule.eta_contraction_rule
                     |> Meson_Clausify.cnf_axiom ctxt new_skolemizer
-                                                (lam_trans = combinatorsN) j
+                                                (lam_trans = combsN) j
                     ||> map do_lams))
              (0 upto length ths0 - 1) ths0
       val ths = maps (snd o snd) th_cls_pairs
       val dischargers = map (fst o snd) th_cls_pairs
       val cls = cls |> map (Drule.eta_contraction_rule #> do_lams)

     if exists_type type_has_top_sort (prop_of st0) then
       verbose_warning ctxt "Proof state contains the universal sort {}"
     else
       ();
     Meson.MESON (preskolem_tac ctxt)
-        (maps (neg_clausify ctxt (lam_trans = combinatorsN))) tac ctxt i st0
+        (maps (neg_clausify ctxt (lam_trans = combsN))) tac ctxt i st0
   end
 
 fun metis_tac [] = generic_metis_tac partial_type_encs
   | metis_tac type_encs = generic_metis_tac type_encs
 

     HEADGOAL (Method.insert_tac nonschem_facts THEN'
               CHANGED_PROP o generic_metis_tac type_encs lam_trans ctxt
                                                (schem_facts @ ths))
   end
 
-val metis_lam_transs = [hide_lamsN, lam_liftingN, combinatorsN]
+val metis_lam_transs = [hide_lamsN, liftingN, combsN]
 
 fun set_opt _ x NONE = SOME x
   | set_opt get x (SOME x0) =
     error ("Cannot specify both " ^ quote (get x0) ^ " and " ^ quote (get x) ^
            ".")