src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML

 
   type minimize_command = string list -> string
   type one_line_params =
     play * string * (string * stature) list * minimize_command * int * int
   type isar_params =
-    bool * bool * Time.time option * real * string Symtab.table
+    bool * bool * Time.time option * bool * real * string Symtab.table
     * (string * stature) list vector * int Symtab.table * string proof * thm
 
   val smtN : string
   val string_for_reconstructor : reconstructor -> string
   val lam_trans_from_atp_proof : string proof -> string -> string

              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 * real * string Symtab.table
+  bool * bool * Time.time option * bool * real * string Symtab.table
   * (string * stature) list vector * int Symtab.table * string proof * thm
 
 fun isar_proof_text ctxt isar_proofs
-    (debug, verbose, preplay_timeout, isar_compress, pool, fact_names, sym_tab,
-     atp_proof, goal)
+    (debug, verbose, preplay_timeout, preplay_trace, isar_compress, pool,
+     fact_names, sym_tab, atp_proof, goal)
     (one_line_params as (_, _, _, _, subgoal, subgoal_count)) =
   let
     val (params, hyp_ts, concl_t) = strip_subgoal ctxt goal subgoal
     val frees = fold Term.add_frees (concl_t :: hyp_ts) []
     val one_line_proof = one_line_proof_text 0 one_line_params

           |> isar_proof_of_direct_proof
           |> (if not preplay andalso isar_compress <= 1.0 then
                 rpair (false, (true, seconds 0.0))
               else
                 compress_and_preplay_proof debug ctxt type_enc lam_trans preplay
-                  preplay_timeout
+                  preplay_timeout preplay_trace
                   (if isar_proofs = SOME true then isar_compress else 1000.0))
           |>> clean_up_labels_in_proof
         val isar_text =
           string_for_proof ctxt type_enc lam_trans subgoal subgoal_count
                            isar_proof