1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Jul 18 08:44:03 2012 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Jul 18 08:44:03 2012 +0200
     1.3 @@ -82,8 +82,8 @@
     1.4     ("strict", "false"),
     1.5     ("lam_trans", "smart"),
     1.6     ("uncurried_aliases", "smart"),
     1.7 -   ("relevance_thresholds", "0.45 0.85"),
     1.8 -   ("max_relevant", "smart"),
     1.9 +   ("fact_thresholds", "0.45 0.85"),
    1.10 +   ("max_facts", "smart"),
    1.11     ("max_mono_iters", "smart"),
    1.12     ("max_new_mono_instances", "smart"),
    1.13     ("isar_proof", "false"),
    1.14 @@ -93,7 +93,8 @@
    1.15     ("preplay_timeout", "3")]
    1.16  
    1.17  val alias_params =
    1.18 -  [("prover", ("provers", [])),
    1.19 +  [("prover", ("provers", [])), (* legacy *)
    1.20 +   ("max_relevant", ("max_facts", [])), (* legacy *)
    1.21     ("dont_preplay", ("preplay_timeout", ["0"]))]
    1.22  val negated_alias_params =
    1.23    [("no_debug", "debug"),
    1.24 @@ -288,8 +289,8 @@
    1.25      val strict = mode = Auto_Try orelse lookup_bool "strict"
    1.26      val lam_trans = lookup_option lookup_string "lam_trans"
    1.27      val uncurried_aliases = lookup_option lookup_bool "uncurried_aliases"
    1.28 -    val relevance_thresholds = lookup_real_pair "relevance_thresholds"
    1.29 -    val max_relevant = lookup_option lookup_int "max_relevant"
    1.30 +    val fact_thresholds = lookup_real_pair "fact_thresholds"
    1.31 +    val max_facts = lookup_option lookup_int "max_facts"
    1.32      val max_mono_iters = lookup_option lookup_int "max_mono_iters"
    1.33      val max_new_mono_instances =
    1.34        lookup_option lookup_int "max_new_mono_instances"
    1.35 @@ -308,7 +309,7 @@
    1.36      {debug = debug, verbose = verbose, overlord = overlord, blocking = blocking,
    1.37       provers = provers, type_enc = type_enc, strict = strict,
    1.38       lam_trans = lam_trans, uncurried_aliases = uncurried_aliases,
    1.39 -     relevance_thresholds = relevance_thresholds, max_relevant = max_relevant,
    1.40 +     fact_thresholds = fact_thresholds, max_facts = max_facts,
    1.41       max_mono_iters = max_mono_iters,
    1.42       max_new_mono_instances = max_new_mono_instances,  isar_proof = isar_proof,
    1.43       isar_shrink_factor = isar_shrink_factor, slice = slice,
    1.44 @@ -405,12 +406,12 @@
    1.45  val parse_params = Scan.optional (Args.bracks (Parse.list parse_param)) []
    1.46  val parse_fact_refs =
    1.47    Scan.repeat1 (Scan.unless (Parse.name -- Args.colon) Parse_Spec.xthm)
    1.48 -val parse_relevance_chunk =
    1.49 +val parse_fact_override_chunk =
    1.50    (Args.add |-- Args.colon |-- parse_fact_refs >> add_fact_override)
    1.51    || (Args.del |-- Args.colon |-- parse_fact_refs >> del_fact_override)
    1.52    || (parse_fact_refs >> only_fact_override)
    1.53  val parse_fact_override =
    1.54 -  Scan.optional (Args.parens (Scan.repeat parse_relevance_chunk
    1.55 +  Scan.optional (Args.parens (Scan.repeat parse_fact_override_chunk
    1.56                                >> merge_fact_overrides))
    1.57                  no_fact_override
    1.58