src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML

    ("verbose", "false"),
    ("overlord", "false"),
    ("blocking", "false"),
    ("type_enc", "smart"),
    ("sound", "false"),
+   ("lam_trans", "smart"),
    ("relevance_thresholds", "0.45 0.85"),
    ("max_relevant", "smart"),
    ("max_mono_iters", "3"),
    ("max_new_mono_instances", "200"),
    ("isar_proof", "false"),

    ("unsound", "sound"),
    ("no_isar_proof", "isar_proof"),
    ("no_slicing", "slicing")]
 
 val params_for_minimize =
-  ["debug", "verbose", "overlord", "type_enc", "sound", "max_mono_iters",
-   "max_new_mono_instances", "isar_proof", "isar_shrink_factor", "timeout",
-   "preplay_timeout"]
+  ["debug", "verbose", "overlord", "type_enc", "sound", "lam_trans",
+   "max_mono_iters", "max_new_mono_instances", "isar_proof",
+   "isar_shrink_factor", "timeout", "preplay_timeout"]
 
 val property_dependent_params = ["provers", "timeout"]
 
 fun is_known_raw_param s =
   AList.defined (op =) default_default_params s orelse

                             | ["true"] => ["false"]
                             | [] => ["false"]
                             | _ => value)
     | NONE => (name, value)
 
-(* "provers =" and "type_enc =" can be left out. The latter is a secret
-   feature. *)
+val any_type_enc = type_enc_from_string Sound "erased"
+
+(* "provers =", "type_enc =", and "lam_trans" can be omitted. For the last two,
+   this is a secret feature. *)
 fun normalize_raw_param ctxt =
   unalias_raw_param
   #> (fn (name, value) =>
          if is_known_raw_param name then
            (name, value)
          else if is_prover_list ctxt name andalso null value then
            ("provers", [name])
          else if can (type_enc_from_string Sound) name andalso null value then
            ("type_enc", [name])
+         else if can (trans_lams_from_string ctxt any_type_enc) name andalso
+                 null value then
+           ("lam_trans", [name])
          else
            error ("Unknown parameter: " ^ quote name ^ "."))
 
 
 (* Ensures that type encodings such as "mono_simple?" and "poly_guards!!" are

         NONE
       else case lookup_string "type_enc" of
         "smart" => NONE
       | s => (type_enc_from_string Sound s; SOME s)
     val sound = mode = Auto_Try orelse lookup_bool "sound"
+    val lam_trans = lookup_string "lam_trans"
     val relevance_thresholds = lookup_real_pair "relevance_thresholds"
     val max_relevant = lookup_option lookup_int "max_relevant"
     val max_mono_iters = lookup_int "max_mono_iters"
     val max_new_mono_instances = lookup_int "max_new_mono_instances"
     val isar_proof = lookup_bool "isar_proof"

       if mode = Auto_Try then Time.zeroTime
       else lookup_time "preplay_timeout" |> the_timeout
     val expect = lookup_string "expect"
   in
     {debug = debug, verbose = verbose, overlord = overlord, blocking = blocking,
-     provers = provers, relevance_thresholds = relevance_thresholds,
+     provers = provers, type_enc = type_enc, sound = sound,
+     lam_trans = lam_trans, relevance_thresholds = relevance_thresholds,
      max_relevant = max_relevant, max_mono_iters = max_mono_iters,
-     max_new_mono_instances = max_new_mono_instances, type_enc = type_enc,
-     sound = sound, isar_proof = isar_proof,
+     max_new_mono_instances = max_new_mono_instances,  isar_proof = isar_proof,
      isar_shrink_factor = isar_shrink_factor, slicing = slicing,
      timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}
   end
 
 fun get_params mode = extract_params mode o default_raw_params