1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Jul 18 08:44:04 2012 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Jul 18 08:44:04 2012 +0200
     1.3 @@ -84,8 +84,9 @@
     1.4     ("strict", "false"),
     1.5     ("lam_trans", "smart"),
     1.6     ("uncurried_aliases", "smart"),
     1.7 +   ("fact_filter", "smart"),
     1.8 +   ("max_facts", "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 @@ -147,8 +148,8 @@
    1.15  
    1.16  val any_type_enc = type_enc_from_string Strict "erased"
    1.17  
    1.18 -(* "provers =", "type_enc =", and "lam_trans" can be omitted. For the last two,
    1.19 -   this is a secret feature. *)
    1.20 +(* "provers =", "type_enc =", "lam_trans =", and "fact_filter =" can be omitted.
    1.21 +   For the last three, this is a secret feature. *)
    1.22  fun normalize_raw_param ctxt =
    1.23    unalias_raw_param
    1.24    #> (fn (name, value) =>
    1.25 @@ -161,6 +162,8 @@
    1.26           else if can (trans_lams_from_string ctxt any_type_enc) name andalso
    1.27                   null value then
    1.28             ("lam_trans", [name])
    1.29 +         else if member (op =) fact_filters name then
    1.30 +           ("fact_filter", [name])
    1.31           else
    1.32             error ("Unknown parameter: " ^ quote name ^ "."))
    1.33  
    1.34 @@ -291,8 +294,9 @@
    1.35      val strict = mode = Auto_Try orelse lookup_bool "strict"
    1.36      val lam_trans = lookup_option lookup_string "lam_trans"
    1.37      val uncurried_aliases = lookup_option lookup_bool "uncurried_aliases"
    1.38 +    val fact_filter = lookup_option lookup_string "fact_filter"
    1.39 +    val max_facts = lookup_option lookup_int "max_facts"
    1.40      val fact_thresholds = lookup_real_pair "fact_thresholds"
    1.41 -    val max_facts = lookup_option lookup_int "max_facts"
    1.42      val max_mono_iters = lookup_option lookup_int "max_mono_iters"
    1.43      val max_new_mono_instances =
    1.44        lookup_option lookup_int "max_new_mono_instances"
    1.45 @@ -311,8 +315,8 @@
    1.46      {debug = debug, verbose = verbose, overlord = overlord, blocking = blocking,
    1.47       provers = provers, type_enc = type_enc, strict = strict,
    1.48       lam_trans = lam_trans, uncurried_aliases = uncurried_aliases,
    1.49 -     fact_thresholds = fact_thresholds, max_facts = max_facts,
    1.50 -     max_mono_iters = max_mono_iters,
    1.51 +     fact_filter = fact_filter, max_facts = max_facts,
    1.52 +     fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters,
    1.53       max_new_mono_instances = max_new_mono_instances,  isar_proof = isar_proof,
    1.54       isar_shrink_factor = isar_shrink_factor, slice = slice,
    1.55       minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout,