src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML

     {outcome: failure option,
      used_facts: (string * locality) list,
      run_time_in_msecs: int option,
      message: string}
 
-  type prover = params -> minimize_command -> prover_problem -> prover_result
+  type prover =
+    params -> (string -> minimize_command) -> prover_problem -> prover_result
 
   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

   {outcome: failure option,
    message: string,
    used_facts: (string * locality) list,
    run_time_in_msecs: int option}
 
-type prover = params -> minimize_command -> prover_problem -> prover_result
+type prover =
+  params -> (string -> minimize_command) -> prover_problem -> prover_result
 
 
 (* configuration attributes *)
 
 val dest_dir =

                    (if is_type_sys_fairly_sound type_sys then Preds else Tags)
                        stuff
                  | _ => type_sys)
      | format => (format, type_sys))
 
-fun determine_format_and_type_sys _ formats (Dumb_Type_Sys type_sys) =
+fun choose_format_and_type_sys _ formats (Dumb_Type_Sys type_sys) =
     adjust_dumb_type_sys formats type_sys
-  | determine_format_and_type_sys best_type_systems formats
-                                  (Smart_Type_Sys full_types) =
+  | choose_format_and_type_sys best_type_systems formats
+                               (Smart_Type_Sys full_types) =
     map type_sys_from_string best_type_systems @ fallback_best_type_systems
     |> find_first (if full_types then is_type_sys_virtually_sound else K true)
     |> the |> adjust_dumb_type_sys formats
+
+val metis_minimize_max_time = seconds 2.0
+
+fun choose_minimize_command minimize_command name preplay =
+  (case preplay of
+     Played (reconstructor, time) =>
+     if Time.<= (time, metis_minimize_max_time) then
+       reconstructor_name reconstructor
+     else
+       name
+   | _ => name)
+  |> minimize_command
 
 fun repair_smt_monomorph_context debug max_mono_iters max_mono_instances =
   Config.put SMT_Config.verbose debug
   #> Config.put SMT_Config.monomorph_full false
   #> Config.put SMT_Config.monomorph_limit max_mono_iters

               let
                 val num_facts =
                   length facts |> is_none max_relevant
                                   ? Integer.min best_max_relevant
                 val (format, type_sys) =
-                  determine_format_and_type_sys best_type_systems formats
-                                                type_sys
+                  choose_format_and_type_sys best_type_systems formats type_sys
                 val fairly_sound = is_type_sys_fairly_sound type_sys
                 val facts =
                   facts |> not fairly_sound
                            ? filter_out (is_dangerous_prop ctxt o prop_of o snd
                                          o untranslated_fact)

             (debug, full_types, isar_shrink_factor, type_sys, pool,
              conjecture_shape, facts_offset, fact_names, sym_tab, atp_proof,
              goal)
           val one_line_params =
             (preplay, proof_banner mode blocking name, used_facts,
-             minimize_command, subgoal, subgoal_count)
+             choose_minimize_command minimize_command name preplay,
+             subgoal, subgoal_count)
         in
           (proof_text ctxt isar_proof isar_params one_line_params ^
            (if verbose then
               "\nATP real CPU time: " ^
               string_from_time (Time.fromMilliseconds (the msecs)) ^ "."

                                      subgoal [Metis, MetisFT] of
               p as Played _ => p
             | _ => Trust_Playable (SMT (smt_settings ()), NONE)
           val one_line_params =
             (preplay, proof_banner mode blocking name, used_facts,
-             minimize_command, subgoal, subgoal_count)
+             choose_minimize_command minimize_command name preplay,
+             subgoal, subgoal_count)
         in
           one_line_proof_text one_line_params ^
           (if verbose then
              "\nSMT solver real CPU time: " ^
              string_from_time (Time.fromMilliseconds (the run_time_in_msecs)) ^

                              [reconstructor] of
       play as Played (_, time) =>
       let
         val one_line_params =
           (play, proof_banner mode blocking name, used_facts,
-           minimize_command, subgoal, subgoal_count)
+           minimize_command name, subgoal, subgoal_count)
       in
         {outcome = NONE, used_facts = used_facts,
          run_time_in_msecs = SOME (Time.toMilliseconds time),
          message = one_line_proof_text one_line_params}
       end