src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML

   type 'a proof = 'a ATP_Proof.proof
   type stature = ATP_Problem_Generate.stature
   type one_line_params = Sledgehammer_Print.one_line_params
 
   type isar_params =
-    bool * bool * Time.time option * bool * real * int * real
+    bool * bool * Time.time option * bool * real * int * real * bool * bool
     * string Symtab.table * (string * stature) list vector
     * (string * term) list * int Symtab.table * string proof * thm
 
   val lam_trans_of_atp_proof : string proof -> string -> string
   val is_typed_helper_used_in_atp_proof : string proof -> bool

              chain_steps (try (List.last #> fst) assms) steps)
     and chain_proofs proofs = map (chain_proof) proofs
   in chain_proof end
 
 type isar_params =
-  bool * bool * Time.time option * bool * real * int * real
+  bool * bool * Time.time option * bool * real * int * real * bool * bool
   * string Symtab.table * (string * stature) list vector
   * (string * term) list * int Symtab.table * string proof * thm
 
 fun isar_proof_text ctxt isar_proofs
     (debug, verbose, preplay_timeout, preplay_trace, isar_compress,
-     isar_compress_degree, merge_timeout_slack, pool, fact_names, lifted,
-     sym_tab, atp_proof, goal)
+     isar_compress_degree, merge_timeout_slack, isar_try0, isar_minimize, pool,
+     fact_names, lifted, sym_tab, atp_proof, goal)
     (one_line_params as (_, _, _, _, subgoal, subgoal_count)) =
   let
     val (params, hyp_ts, concl_t) = strip_subgoal goal subgoal ctxt
     val (_, ctxt) =
       params

           isar_proof
           |> compress_proof
                (if isar_proofs = SOME true then isar_compress else 1000.0)
                (if isar_proofs = SOME true then isar_compress_degree else 100)
                merge_timeout_slack preplay_interface
-          |> try0 preplay_timeout preplay_interface
-          |> minimize_dependencies_and_remove_unrefed_steps preplay_interface
+          |> isar_try0 ? try0 preplay_timeout preplay_interface
+          |> minimize_dependencies_and_remove_unrefed_steps isar_minimize
+               preplay_interface
           |> `overall_preplay_stats
           ||> clean_up_labels_in_proof
         val isar_text = string_of_proof ctxt type_enc lam_trans subgoal
           subgoal_count isar_proof
       in