--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Wed Aug 24 11:17:33 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Wed Aug 24 15:25:39 2011 +0200
@@ -57,16 +57,16 @@
(if verbose then " (timeout: " ^ string_from_time timeout ^ ")"
else "") ^ "...")
val {goal, ...} = Proof.goal state
+ val facts =
+ facts |> maps (fn (n, ths) => ths |> map (Untranslated_Fact o pair n))
val params =
{debug = debug, verbose = verbose, overlord = overlord, blocking = true,
provers = provers, type_enc = type_enc, sound = true,
- relevance_thresholds = (1.01, 1.01), max_relevant = NONE,
+ relevance_thresholds = (1.01, 1.01), max_relevant = SOME (length facts),
max_mono_iters = max_mono_iters,
max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof,
isar_shrink_factor = isar_shrink_factor, slicing = false,
timeout = timeout, preplay_timeout = preplay_timeout, expect = ""}
- val facts =
- facts |> maps (fn (n, ths) => ths |> map (Untranslated_Fact o pair n))
val problem =
{state = state, goal = goal, subgoal = i, subgoal_count = n,
facts = facts, smt_filter = NONE}