1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Aug 25 09:42:28 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Aug 25 17:49:52 2010 +0200
     1.3 @@ -68,8 +68,8 @@
     1.4     ("overlord", "false"),
     1.5     ("explicit_apply", "false"),
     1.6     ("relevance_threshold", "40"),
     1.7 -   ("relevance_decay", "31"),
     1.8 -   ("max_relevant_per_iter", "smart"),
     1.9 +   ("relevance_decay", "smart"),
    1.10 +   ("max_relevant", "smart"),
    1.11     ("theory_relevant", "smart"),
    1.12     ("isar_proof", "false"),
    1.13     ("isar_shrink_factor", "1")]
    1.14 @@ -169,8 +169,9 @@
    1.15      val relevance_threshold =
    1.16        0.01 * Real.fromInt (lookup_int "relevance_threshold")
    1.17      val relevance_decay =
    1.18 -      0.01 * Real.fromInt (lookup_int "relevance_decay")
    1.19 -    val max_relevant_per_iter = lookup_int_option "max_relevant_per_iter"
    1.20 +      lookup_int_option "relevance_decay"
    1.21 +      |> Option.map (fn n => 0.01 * Real.fromInt n)
    1.22 +    val max_relevant = lookup_int_option "max_relevant"
    1.23      val theory_relevant = lookup_bool_option "theory_relevant"
    1.24      val isar_proof = lookup_bool "isar_proof"
    1.25      val isar_shrink_factor = Int.max (1, lookup_int "isar_shrink_factor")
    1.26 @@ -179,8 +180,7 @@
    1.27      {debug = debug, verbose = verbose, overlord = overlord, atps = atps,
    1.28       full_types = full_types, explicit_apply = explicit_apply,
    1.29       relevance_threshold = relevance_threshold,
    1.30 -     relevance_decay = relevance_decay,
    1.31 -     max_relevant_per_iter = max_relevant_per_iter,
    1.32 +     relevance_decay = relevance_decay, max_relevant = max_relevant,
    1.33       theory_relevant = theory_relevant, isar_proof = isar_proof,
    1.34       isar_shrink_factor = isar_shrink_factor, timeout = timeout}
    1.35    end