--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Fri Sep 20 22:39:30 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Fri Sep 20 22:39:30 2013 +0200
@@ -37,7 +37,6 @@
isar_proofs : bool option,
isar_compress : real,
isar_compress_degree : int,
- merge_timeout_slack : real,
isar_try0 : bool,
isar_minimize : bool,
slice : bool,
@@ -351,7 +350,6 @@
isar_proofs : bool option,
isar_compress : real,
isar_compress_degree : int,
- merge_timeout_slack : real,
isar_try0 : bool,
isar_minimize : bool,
slice : bool,
@@ -679,8 +677,8 @@
(params as {debug, verbose, overlord, type_enc, strict, lam_trans,
uncurried_aliases, fact_filter, max_facts, max_mono_iters,
max_new_mono_instances, isar_proofs, isar_compress,
- isar_compress_degree, merge_timeout_slack, isar_try0,
- isar_minimize, slice, timeout, preplay_timeout, ...})
+ isar_compress_degree, isar_try0, isar_minimize, slice,
+ timeout, preplay_timeout, ...})
minimize_command
({state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) =
let
@@ -956,9 +954,8 @@
()
val isar_params =
(debug, verbose, preplay_timeout, isar_compress,
- isar_compress_degree, merge_timeout_slack, isar_try0,
- isar_minimize, pool, fact_names, lifted, sym_tab, atp_proof,
- goal)
+ isar_compress_degree, isar_try0, isar_minimize, pool,
+ fact_names, lifted, sym_tab, atp_proof, goal)
val one_line_params =
(preplay, proof_banner mode name, used_facts,
choose_minimize_command ctxt params minimize_command name