src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML

 val prover_timeoutK = "prover_timeout"
 val keepK = "keep"
 val type_encK = "type_enc"
 val soundK = "sound"
 val slicingK = "slicing"
-val lambda_transK = "lambda_trans"
+val lam_transK = "lam_trans"
 val e_weight_methodK = "e_weight_method"
 val force_sosK = "force_sos"
 val max_relevantK = "max_relevant"
 val max_callsK = "max_calls"
 val minimizeK = "minimize"

 datatype sh_result =
   SH_OK of int * int * (string * locality) list |
   SH_FAIL of int * int |
   SH_ERROR
 
-fun run_sh prover_name prover type_enc sound max_relevant slicing lambda_trans
+fun run_sh prover_name prover type_enc sound max_relevant slicing lam_trans
         e_weight_method force_sos hard_timeout timeout dir pos st =
   let
     val {context = ctxt, facts = chained_ths, goal} = Proof.goal st
     val i = 1
     fun set_file_name (SOME dir) =

           ^ serial_string ())
       | set_file_name NONE = I
     val st' =
       st |> Proof.map_context
                 (set_file_name dir
-                 #> (Option.map (Config.put
-                       Sledgehammer_Provers.atp_lambda_trans)
-                       lambda_trans |> the_default I)
                  #> (Option.map (Config.put ATP_Systems.e_weight_method)
                        e_weight_method |> the_default I)
                  #> (Option.map (Config.put ATP_Systems.force_sos)
                        force_sos |> the_default I))
     val params as {relevance_thresholds, max_relevant, slicing, ...} =
       Sledgehammer_Isar.default_params ctxt
           [("verbose", "true"),
            ("type_enc", type_enc),
            ("sound", sound),
+           ("lam_trans", lam_trans |> the_default "smart"),
            ("preplay_timeout", preplay_timeout),
            ("max_relevant", max_relevant),
            ("slicing", slicing),
            ("timeout", string_of_int timeout),
            ("preplay_timeout", preplay_timeout)]

     val (prover_name, prover) = get_prover (Proof.context_of st) args
     val type_enc = AList.lookup (op =) args type_encK |> the_default "smart"
     val sound = AList.lookup (op =) args soundK |> the_default "false"
     val max_relevant = AList.lookup (op =) args max_relevantK |> the_default "smart"
     val slicing = AList.lookup (op =) args slicingK |> the_default "true"
-    val lambda_trans = AList.lookup (op =) args lambda_transK
+    val lam_trans = AList.lookup (op =) args lam_transK
     val e_weight_method = AList.lookup (op =) args e_weight_methodK
     val force_sos = AList.lookup (op =) args force_sosK
       |> Option.map (curry (op <>) "false")
     val dir = AList.lookup (op =) args keepK
     val timeout = Mirabelle.get_int_setting args (prover_timeoutK, 30)
     (* always use a hard timeout, but give some slack so that the automatic
        minimizer has a chance to do its magic *)
     val hard_timeout = SOME (2 * timeout)
     val (msg, result) =
-      run_sh prover_name prover type_enc sound max_relevant slicing lambda_trans
+      run_sh prover_name prover type_enc sound max_relevant slicing lam_trans
         e_weight_method force_sos hard_timeout timeout dir pos st
   in
     case result of
       SH_OK (time_isa, time_prover, names) =>
         let

         if !reconstructor = "sledgehammer_tac" then
           sledge_tac 0.2 ATP_Systems.z3_tptpN "mono_simple"
           ORELSE' sledge_tac 0.2 ATP_Systems.eN "mono_guards??"
           ORELSE' sledge_tac 0.2 ATP_Systems.vampireN "mono_guards??"
           ORELSE' sledge_tac 0.2 ATP_Systems.spassN "poly_tags"
-          ORELSE' Metis_Tactic.metis_tac [] ctxt thms
+          ORELSE' Metis_Tactic.metis_tac [] ATP_Translate.combinatorsN ctxt thms
         else if !reconstructor = "smt" then
           SMT_Solver.smt_tac ctxt thms
         else if full orelse !reconstructor = "metis (full_types)" then
-          Metis_Tactic.metis_tac [Metis_Tactic.full_type_enc] ctxt thms
+          Metis_Tactic.metis_tac [Metis_Tactic.full_type_enc]
+                                 ATP_Translate.combinatorsN ctxt thms
         else if !reconstructor = "metis (no_types)" then
-          Metis_Tactic.metis_tac [Metis_Tactic.no_type_enc] ctxt thms
+          Metis_Tactic.metis_tac [Metis_Tactic.no_type_enc]
+                                 ATP_Translate.combinatorsN ctxt thms
         else if !reconstructor = "metis" then
-          Metis_Tactic.metis_tac [] ctxt thms
+          Metis_Tactic.metis_tac [] ATP_Translate.combinatorsN ctxt thms
         else
           K all_tac
       end
     fun apply_reconstructor named_thms =
       Mirabelle.can_apply timeout (do_reconstructor named_thms) st