# HG changeset patch
# User blanchet
# Date 1342815586 -7200
# Node ID 9fe826095a027848a2d32615fb50a0e0b8a5eeed
# Parent  dd82d190c2af0325279ea8c5b40ff209768e3b9c
convenience

diff -r dd82d190c2af -r 9fe826095a02 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jul 20 22:19:46 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jul 20 22:19:46 2012 +0200
@@ -151,8 +151,8 @@
 
 val any_type_enc = type_enc_from_string Strict "erased"
 
-(* "provers =", "type_enc =", "lam_trans =", and "fact_filter =" can be omitted.
-   For the last three, this is a secret feature. *)
+(* "provers =", "type_enc =", "lam_trans =", "fact_filter =", and "max_facts ="
+   can be omitted. For the last four, this is a secret feature. *)
 fun normalize_raw_param ctxt =
   unalias_raw_param
   #> (fn (name, value) =>
@@ -167,8 +167,9 @@
            ("lam_trans", [name])
          else if member (op =) fact_filters name then
            ("fact_filter", [name])
-         else
-           error ("Unknown parameter: " ^ quote name ^ "."))
+         else case Int.fromString name of
+           SOME n => ("max_facts", [name])
+         | NONE => error ("Unknown parameter: " ^ quote name ^ "."))
 
 
 (* Ensures that type encodings such as "mono_native?" and "poly_guards!!" are