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