--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Mon May 06 11:03:08 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Mon May 06 11:03:08 2013 +0200
@@ -57,7 +57,7 @@
fun test_facts ({debug, verbose, overlord, provers, max_mono_iters,
max_new_mono_instances, type_enc, strict, lam_trans,
uncurried_aliases, isar_proofs, isar_compress,
- preplay_timeout, ...} : params)
+ preplay_timeout, preplay_trace, ...} : params)
silent (prover : prover) timeout i n state facts =
let
val _ =
@@ -80,7 +80,8 @@
max_new_mono_instances = max_new_mono_instances,
isar_proofs = isar_proofs, isar_compress = isar_compress,
slice = false, minimize = SOME false, timeout = timeout,
- preplay_timeout = preplay_timeout, expect = ""}
+ preplay_timeout = preplay_timeout, preplay_trace = preplay_trace,
+ expect = ""}
val problem =
{state = state, goal = goal, subgoal = i, subgoal_count = n,
factss = [("", facts)]}
@@ -250,8 +251,8 @@
({debug, verbose, overlord, blocking, provers, type_enc, strict,
lam_trans, uncurried_aliases, learn, fact_filter, max_facts,
fact_thresholds, max_mono_iters, max_new_mono_instances, isar_proofs,
- isar_compress, slice, minimize, timeout, preplay_timeout, expect}
- : params) =
+ isar_compress, slice, minimize, timeout, preplay_timeout,
+ preplay_trace, expect} : params) =
let
fun lookup_override name default_value =
case AList.lookup (op =) override_params name of
@@ -269,7 +270,8 @@
fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters,
max_new_mono_instances = max_new_mono_instances, isar_proofs = isar_proofs,
isar_compress = isar_compress, slice = slice, minimize = minimize,
- timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}
+ timeout = timeout, preplay_timeout = preplay_timeout,
+ preplay_trace = preplay_trace, expect = expect}
end
fun maybe_minimize ctxt mode do_learn name