1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu Jul 26 10:48:03 2012 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu Jul 26 11:07:27 2012 +0200
     1.3 @@ -162,21 +162,22 @@
     1.4    #> (fn (name, value) =>
     1.5           if is_known_raw_param name then
     1.6             (name, value)
     1.7 -         else if is_prover_list ctxt name andalso null value then
     1.8 -           ("provers", [name])
     1.9 -         else if can (type_enc_from_string Strict) name andalso null value then
    1.10 -           ("type_enc", [name])
    1.11 -         else if can (trans_lams_from_string ctxt any_type_enc) name andalso
    1.12 -                 null value then
    1.13 -           ("lam_trans", [name])
    1.14 -         else if member (op =) fact_filters name then
    1.15 -           ("fact_filter", [name])
    1.16 -         else if can Int.fromString name then
    1.17 -           ("max_facts", [name])
    1.18 +         else if null value then
    1.19 +           if is_prover_list ctxt name then
    1.20 +             ("provers", [name])
    1.21 +           else if can (type_enc_from_string Strict) name then
    1.22 +             ("type_enc", [name])
    1.23 +           else if can (trans_lams_from_string ctxt any_type_enc) name then
    1.24 +             ("lam_trans", [name])
    1.25 +           else if member (op =) fact_filters name then
    1.26 +             ("fact_filter", [name])
    1.27 +           else if is_some (Int.fromString name) then
    1.28 +             ("max_facts", [name])
    1.29 +           else
    1.30 +             error ("Unknown parameter: " ^ quote name ^ ".")
    1.31           else
    1.32             error ("Unknown parameter: " ^ quote name ^ "."))
    1.33  
    1.34 -
    1.35  (* Ensures that type encodings such as "mono_native?" and "poly_guards!!" are
    1.36     read correctly. *)
    1.37  val implode_param = strip_spaces_except_between_idents o space_implode " "