1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jul 20 22:19:46 2012 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jul 20 22:19:46 2012 +0200
     1.3 @@ -151,8 +151,8 @@
     1.4  
     1.5  val any_type_enc = type_enc_from_string Strict "erased"
     1.6  
     1.7 -(* "provers =", "type_enc =", "lam_trans =", and "fact_filter =" can be omitted.
     1.8 -   For the last three, this is a secret feature. *)
     1.9 +(* "provers =", "type_enc =", "lam_trans =", "fact_filter =", and "max_facts ="
    1.10 +   can be omitted. For the last four, this is a secret feature. *)
    1.11  fun normalize_raw_param ctxt =
    1.12    unalias_raw_param
    1.13    #> (fn (name, value) =>
    1.14 @@ -167,8 +167,9 @@
    1.15             ("lam_trans", [name])
    1.16           else if member (op =) fact_filters name then
    1.17             ("fact_filter", [name])
    1.18 -         else
    1.19 -           error ("Unknown parameter: " ^ quote name ^ "."))
    1.20 +         else case Int.fromString name of
    1.21 +           SOME n => ("max_facts", [name])
    1.22 +         | NONE => error ("Unknown parameter: " ^ quote name ^ "."))
    1.23  
    1.24  
    1.25  (* Ensures that type encodings such as "mono_native?" and "poly_guards!!" are