--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML Wed Aug 25 17:49:52 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML Wed Aug 25 19:41:18 2010 +0200
@@ -50,7 +50,7 @@
val params =
{debug = debug, verbose = verbose, overlord = overlord, atps = atps,
full_types = full_types, explicit_apply = explicit_apply,
- relevance_threshold = 1.1, relevance_decay = NONE, max_relevant = NONE,
+ relevance_thresholds = (1.01, 1.01), max_relevant = NONE,
theory_relevant = NONE, isar_proof = isar_proof,
isar_shrink_factor = isar_shrink_factor, timeout = timeout}
val axioms = maps (fn (n, ths) => map (pair n) ths) axioms