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 @@ -167,9 +167,10 @@
     1.4             ("lam_trans", [name])
     1.5           else if member (op =) fact_filters name then
     1.6             ("fact_filter", [name])
     1.7 -         else case Int.fromString name of
     1.8 -           SOME n => ("max_facts", [name])
     1.9 -         | NONE => error ("Unknown parameter: " ^ quote name ^ "."))
    1.10 +         else if can Int.fromString name then
    1.11 +           ("max_facts", [name])
    1.12 +         else
    1.13 +           error ("Unknown parameter: " ^ quote name ^ "."))
    1.14  
    1.15  
    1.16  (* Ensures that type encodings such as "mono_native?" and "poly_guards!!" are
    1.17 @@ -375,7 +376,7 @@
    1.18        let
    1.19          val ctxt = ctxt |> Config.put instantiate_inducts false
    1.20          val i = the_default 1 opt_i
    1.21 -        val params as {provers, ...} =
    1.22 +        val params =
    1.23            get_params Minimize ctxt (("provers", [default_minimize_prover]) ::
    1.24                                      override_params)
    1.25          val goal = prop_of (#goal (Proof.goal state))