--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Fri Jul 12 21:14:54 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Fri Jul 12 22:41:25 2013 +0200
@@ -12,7 +12,7 @@
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
@@ -409,14 +409,14 @@
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
@@ -594,8 +594,9 @@
(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