src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML

    ("isar_proofs", "smart"),
    ("compress", "10"),
    ("try0", "true"),
    ("smt_proofs", "smart"),
    ("slice", "true"),
-   ("minimize", "smart"),
+   ("minimize", "true"),
    ("preplay_timeout", "1")]
 
 val alias_params =
   [("prover", ("provers", [])), (* undocumented *)
    ("dont_preplay", ("preplay_timeout", ["0"])),

     val isar_proofs = lookup_option lookup_bool "isar_proofs"
     val compress = Real.max (1.0, lookup_real "compress")
     val try0 = lookup_bool "try0"
     val smt_proofs = lookup_option lookup_bool "smt_proofs"
     val slice = mode <> Auto_Try andalso lookup_bool "slice"
-    val minimize = if mode = Auto_Try then NONE else lookup_option lookup_bool "minimize"
+    val minimize = mode <> Auto_Try andalso lookup_bool "minimize"
     val timeout = lookup_time "timeout"
     val preplay_timeout = if mode = Auto_Try then Time.zeroTime else lookup_time "preplay_timeout"
     val expect = lookup_string "expect"
   in
     {debug = debug, verbose = verbose, overlord = overlord, spy = spy, blocking = blocking,

            (* TODO: Use MaSh mode instead and have the special defaults hardcoded in "get_params" *)
            (get_params Normal thy
                 ([("timeout", [string_of_real default_learn_prover_timeout]),
                   ("slice", ["false"])] @
                  override_params @
-                 [("minimize", ["true"]),
-                  ("preplay_timeout", ["0"])]))
+                 [("preplay_timeout", ["0"])]))
            fact_override (#facts (Proof.goal state))
            (subcommand = learn_proverN orelse subcommand = relearn_proverN))
     else if subcommand = running_learnersN then
       running_learners ()
     else if subcommand = refresh_tptpN then

 
           val override_params =
             ((if provers_arg = "" then [] else [("provers", space_explode " " provers_arg)]) @
               [("isar_proofs", [isar_proofs_arg]),
                ("blocking", ["true"]),
-               ("minimize", ["true"]),
                ("debug", ["false"]),
                ("verbose", ["false"]),
                ("overlord", ["false"])])
             |> map (normalize_raw_param ctxt)