src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML

 val uncurried_aliasesK = "uncurried_aliases"
 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"
+val minimizeK = "minimize" (*refers to minimization attempted by Mirabelle*)
 val minimize_timeoutK = "minimize_timeout"
 val metis_ftK = "metis_ft"
 val reconstructorK = "reconstructor"
-
-val preplay_timeout = "4"
+val preplay_timeoutK = "preplay_timeout"
+val sh_minimizeK = "sh_minimize" (*refers to minimizer run within Sledgehammer*)
 
 fun sh_tag id = "#" ^ string_of_int id ^ " sledgehammer: "
 fun minimize_tag id = "#" ^ string_of_int id ^ " minimize (sledgehammer): "
 fun reconstructor_tag reconstructor id =
   "#" ^ string_of_int id ^ " " ^ (!reconstructor) ^ " (sledgehammer): "
 
 val separator = "-----"
 
+val preplay_timeout_default = "4"
 
 datatype sh_data = ShData of {
   calls: int,
   success: int,
   nontriv_calls: int,

   SH_OK of int * int * (string * stature) list |
   SH_FAIL of int * int |
   SH_ERROR
 
 fun run_sh prover_name prover type_enc strict max_relevant slice lam_trans
-        uncurried_aliases e_weight_method force_sos hard_timeout timeout dir pos
-        st =
+        uncurried_aliases e_weight_method force_sos hard_timeout timeout
+        preplay_timeout sh_minimize dir pos st =
   let
     val {context = ctxt, facts = chained_ths, goal} = Proof.goal st
     val i = 1
     fun set_file_name (SOME dir) =
         Config.put Sledgehammer_Provers.dest_dir dir

            ("lam_trans", lam_trans |> the_default "smart"),
            ("uncurried_aliases", uncurried_aliases |> the_default "smart"),
            ("max_relevant", max_relevant),
            ("slice", slice),
            ("timeout", string_of_int timeout),
+           ("minimize", sh_minimize), (*don't confuse the two minimization flags*)
            ("preplay_timeout", preplay_timeout)]
     val default_max_relevant =
       Sledgehammer_Provers.default_max_relevant_for_prover ctxt slice
         prover_name
     val is_appropriate_prop =

       |> 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 preplay_timeout = AList.lookup (op =) args preplay_timeoutK
+      |> the_default preplay_timeout_default
+    val sh_minimize = AList.lookup (op =) args sh_minimizeK |> the_default "smart"
     val hard_timeout = SOME (2 * timeout)
     val (msg, result) =
       run_sh prover_name prover type_enc strict max_relevant slice lam_trans
-        uncurried_aliases e_weight_method force_sos hard_timeout timeout dir pos
-        st
+        uncurried_aliases e_weight_method force_sos hard_timeout timeout
+        preplay_timeout sh_minimize dir pos st
   in
     case result of
       SH_OK (time_isa, time_prover, names) =>
         let
           fun get_thms (name, stature) =

     val strict = AList.lookup (op =) args strictK |> the_default "false"
     val timeout =
       AList.lookup (op =) args minimize_timeoutK
       |> Option.map (fst o read_int o raw_explode)  (* FIXME Symbol.explode (?) *)
       |> the_default 5
+    val preplay_timeout = AList.lookup (op =) args preplay_timeoutK
+      |> the_default preplay_timeout_default
+    val sh_minimize = AList.lookup (op =) args sh_minimizeK |> the_default "smart"
     val params = Sledgehammer_Isar.default_params ctxt
       [("provers", prover_name),
        ("verbose", "true"),
        ("type_enc", type_enc),
        ("strict", strict),
        ("timeout", string_of_int timeout),
-       ("preplay_timeout", preplay_timeout)]
+       ("preplay_timeout", preplay_timeout),
+       ("minimize", sh_minimize)] (*don't confuse the two minimization flags*)
     val minimize =
       Sledgehammer_Minimize.minimize_facts prover_name params
           true 1 (Sledgehammer_Util.subgoal_count st)
     val _ = log separator
     val (used_facts, (preplay, message, message_tail)) =