--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Wed Jul 18 08:44:03 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Wed Jul 18 08:44:03 2012 +0200
@@ -68,7 +68,7 @@
{debug = debug, verbose = verbose, overlord = overlord, blocking = true,
provers = provers, type_enc = type_enc, strict = strict,
lam_trans = lam_trans, uncurried_aliases = uncurried_aliases,
- relevance_thresholds = (1.01, 1.01), max_relevant = SOME (length facts),
+ fact_thresholds = (1.01, 1.01), max_facts = 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, slice = false,
@@ -225,7 +225,7 @@
fun adjust_reconstructor_params override_params
({debug, verbose, overlord, blocking, provers, type_enc, strict,
- lam_trans, uncurried_aliases, relevance_thresholds, max_relevant,
+ lam_trans, uncurried_aliases, fact_thresholds, max_facts,
max_mono_iters, max_new_mono_instances, isar_proof, isar_shrink_factor,
slice, minimize, timeout, preplay_timeout, expect} : params) =
let
@@ -241,7 +241,7 @@
{debug = debug, verbose = verbose, overlord = overlord, blocking = blocking,
provers = provers, type_enc = type_enc, strict = strict,
lam_trans = lam_trans, uncurried_aliases = uncurried_aliases,
- max_relevant = max_relevant, relevance_thresholds = relevance_thresholds,
+ max_facts = max_facts, fact_thresholds = fact_thresholds,
max_mono_iters = max_mono_iters,
max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof,
isar_shrink_factor = isar_shrink_factor, slice = slice,
@@ -304,8 +304,8 @@
case used_facts of
SOME used_facts =>
(if debug andalso not (null used_facts) then
- facts ~~ (0 upto length facts - 1)
- |> map (fn (fact, j) => fact |> untranslated_fact |> apsnd (K j))
+ tag_list 1 facts
+ |> map (fn (j, fact) => fact |> untranslated_fact |> apsnd (K j))
|> filter_used_facts used_facts
|> map (fn ((name, _), j) => name ^ "@" ^ string_of_int j)
|> commas