--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Aug 25 09:42:28 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Wed Aug 25 17:49:52 2010 +0200
@@ -68,8 +68,8 @@
("overlord", "false"),
("explicit_apply", "false"),
("relevance_threshold", "40"),
- ("relevance_decay", "31"),
- ("max_relevant_per_iter", "smart"),
+ ("relevance_decay", "smart"),
+ ("max_relevant", "smart"),
("theory_relevant", "smart"),
("isar_proof", "false"),
("isar_shrink_factor", "1")]
@@ -169,8 +169,9 @@
val relevance_threshold =
0.01 * Real.fromInt (lookup_int "relevance_threshold")
val relevance_decay =
- 0.01 * Real.fromInt (lookup_int "relevance_decay")
- val max_relevant_per_iter = lookup_int_option "max_relevant_per_iter"
+ lookup_int_option "relevance_decay"
+ |> Option.map (fn n => 0.01 * Real.fromInt n)
+ val max_relevant = lookup_int_option "max_relevant"
val theory_relevant = lookup_bool_option "theory_relevant"
val isar_proof = lookup_bool "isar_proof"
val isar_shrink_factor = Int.max (1, lookup_int "isar_shrink_factor")
@@ -179,8 +180,7 @@
{debug = debug, verbose = verbose, overlord = overlord, atps = atps,
full_types = full_types, explicit_apply = explicit_apply,
relevance_threshold = relevance_threshold,
- relevance_decay = relevance_decay,
- max_relevant_per_iter = max_relevant_per_iter,
+ relevance_decay = relevance_decay, max_relevant = max_relevant,
theory_relevant = theory_relevant, isar_proof = isar_proof,
isar_shrink_factor = isar_shrink_factor, timeout = timeout}
end