src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML

      overlord: bool,
      blocking: bool,
      provers: string list,
      type_enc: string option,
      sound: bool,
+     lam_trans: string,
      relevance_thresholds: real * real,
      max_relevant: int option,
      max_mono_iters: int,
      max_new_mono_instances: int,
      isar_proof: bool,

   type prover =
     params -> (string -> minimize_command) -> prover_problem -> prover_result
 
   val dest_dir : string Config.T
   val problem_prefix : string Config.T
-  val atp_lambda_trans : string Config.T
   val atp_full_names : bool Config.T
   val smt_triggers : bool Config.T
   val smt_weights : bool Config.T
   val smt_weight_min_facts : int Config.T
   val smt_min_weight : int Config.T

    overlord: bool,
    blocking: bool,
    provers: string list,
    type_enc: string option,
    sound: bool,
+   lam_trans: string,
    relevance_thresholds: real * real,
    max_relevant: int option,
    max_mono_iters: int,
    max_new_mono_instances: int,
    isar_proof: bool,

 val dest_dir =
   Attrib.setup_config_string @{binding sledgehammer_dest_dir} (K "")
 val problem_prefix =
   Attrib.setup_config_string @{binding sledgehammer_problem_prefix} (K "prob")
 
-val atp_lambda_trans =
-  Attrib.setup_config_string @{binding sledgehammer_atp_lambda_trans} (K smartN)
 (* In addition to being easier to read, readable names are often much shorter,
    especially if types are mangled in names. This makes a difference for some
    provers (e.g., E). For these reason, short names are enabled by default. *)
 val atp_full_names =
   Attrib.setup_config_bool @{binding sledgehammer_atp_full_names} (K false)

     val {context = ctxt, facts, goal} = Proof.goal state
     val full_tac = Method.insert_tac facts i THEN tac ctxt i
   in TimeLimit.timeLimit timeout (try (Seq.pull o full_tac)) goal end
 
 fun tac_for_reconstructor Metis =
-    Metis_Tactic.metis_tac [Metis_Tactic.partial_type_enc]
+    Metis_Tactic.metis_tac [Metis_Tactic.partial_type_enc] combinatorsN
   | tac_for_reconstructor Metis_Full_Types =
-    Metis_Tactic.metis_tac Metis_Tactic.full_type_syss
+    Metis_Tactic.metis_tac Metis_Tactic.full_type_syss combinatorsN
   | tac_for_reconstructor Metis_No_Types =
-    Metis_Tactic.metis_tac [Metis_Tactic.no_type_enc]
+    Metis_Tactic.metis_tac [Metis_Tactic.no_type_enc] combinatorsN
   | tac_for_reconstructor SMT = SMT_Solver.smt_tac
 
 fun timed_reconstructor reconstructor debug timeout ths =
   (Config.put Metis_Tactic.verbose debug
    #> (fn ctxt => tac_for_reconstructor reconstructor ctxt ths))

 val atp_timeout_slack = seconds 1.0
 
 fun run_atp mode name
         ({exec, required_execs, arguments, proof_delims, known_failures,
           conj_sym_kind, prem_kind, best_slices, ...} : atp_config)
-        ({debug, verbose, overlord, type_enc, sound, max_relevant,
+        ({debug, verbose, overlord, type_enc, sound, lam_trans, max_relevant,
           max_mono_iters, max_new_mono_instances, isar_proof,
           isar_shrink_factor, slicing, timeout, preplay_timeout, ...} : params)
         minimize_command
         ({state, goal, subgoal, subgoal_count, facts, ...} : prover_problem) =
   let

                     plural_s num_facts ^ " for " ^
                     string_from_time slice_timeout ^ "..."
                     |> Output.urgent_message
                   else
                     ()
+                val readable_names = not (Config.get ctxt atp_full_names)
                 val (atp_problem, pool, conjecture_offset, facts_offset,
                      fact_names, typed_helpers, _, sym_tab) =
                   prepare_atp_problem ctxt format conj_sym_kind prem_kind
-                      type_enc false (Config.get ctxt atp_lambda_trans)
-                      (not (Config.get ctxt atp_full_names)) true hyp_ts concl_t
-                      facts
+                      type_enc false lam_trans readable_names true hyp_ts
+                      concl_t facts
                 fun weights () = atp_problem_weights atp_problem
                 val full_proof = debug orelse isar_proof
                 val core =
                   File.shell_path command ^ " " ^
                   arguments ctxt full_proof extra slice_timeout weights ^ " " ^