# 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