src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML

          else if can (trans_lams_from_string ctxt any_type_enc) name andalso
                  null value then
            ("lam_trans", [name])
          else if member (op =) fact_filters name then
            ("fact_filter", [name])
-         else case Int.fromString name of
-           SOME n => ("max_facts", [name])
-         | NONE => error ("Unknown parameter: " ^ quote name ^ "."))
+         else if can Int.fromString name then
+           ("max_facts", [name])
+         else
+           error ("Unknown parameter: " ^ quote name ^ "."))
 
 
 (* Ensures that type encodings such as "mono_native?" and "poly_guards!!" are
    read correctly. *)
 val implode_param = strip_spaces_except_between_idents o space_implode " "

       end
     else if subcommand = minN then
       let
         val ctxt = ctxt |> Config.put instantiate_inducts false
         val i = the_default 1 opt_i
-        val params as {provers, ...} =
+        val params =
           get_params Minimize ctxt (("provers", [default_minimize_prover]) ::
                                     override_params)
         val goal = prop_of (#goal (Proof.goal state))
         val facts = nearly_all_facts ctxt false fact_override Symtab.empty
                                      Termtab.empty [] [] goal