--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Fri Sep 20 22:39:30 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Fri Sep 20 22:39:30 2013 +0200
@@ -12,7 +12,7 @@
type one_line_params = Sledgehammer_Print.one_line_params
type isar_params =
- bool * bool * Time.time option * real * bool * bool * string Symtab.table
+ bool * bool * Time.time option * real * bool * string Symtab.table
* (string * stature) list vector * (string * term) list * int Symtab.table
* string atp_proof * thm
@@ -408,13 +408,13 @@
in chain_proof end
type isar_params =
- bool * bool * Time.time option * real * bool * bool * string Symtab.table
+ bool * bool * Time.time option * real * bool * string Symtab.table
* (string * stature) list vector * (string * term) list * int Symtab.table
* string atp_proof * thm
fun isar_proof_text ctxt isar_proofs
- (debug, verbose, preplay_timeout, isar_compress, isar_try0, isar_minimize,
- pool, fact_names, lifted, sym_tab, atp_proof, goal)
+ (debug, verbose, preplay_timeout, isar_compress, isar_try0, 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
@@ -592,7 +592,7 @@
(if isar_proofs = SOME true then isar_compress else 1000.0)
preplay_interface
|> isar_try0 ? try0 preplay_timeout preplay_interface
- |> minimize_dependencies_and_remove_unrefed_steps isar_minimize
+ |> minimize_dependencies_and_remove_unrefed_steps isar_try0
preplay_interface
|> `overall_preplay_stats
||> clean_up_labels_in_proof