# HG changeset patch
# User blanchet
# Date 1343293647 -7200
# Node ID 5ada9fd7507bdb232ffc1a0f0bba30838e26fe1d
# Parent  c0f44941e674b3541b5dedf5e571659813306232
detect unknown options again

diff -r c0f44941e674 -r 5ada9fd7507b src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu Jul 26 10:48:03 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu Jul 26 11:07:27 2012 +0200
@@ -162,21 +162,22 @@
   #> (fn (name, value) =>
          if is_known_raw_param name then
            (name, value)
-         else if is_prover_list ctxt name andalso null value then
-           ("provers", [name])
-         else if can (type_enc_from_string Strict) name andalso null value then
-           ("type_enc", [name])
-         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 if can Int.fromString name then
-           ("max_facts", [name])
+         else if null value then
+           if is_prover_list ctxt name then
+             ("provers", [name])
+           else if can (type_enc_from_string Strict) name then
+             ("type_enc", [name])
+           else if can (trans_lams_from_string ctxt any_type_enc) name then
+             ("lam_trans", [name])
+           else if member (op =) fact_filters name then
+             ("fact_filter", [name])
+           else if is_some (Int.fromString name) then
+             ("max_facts", [name])
+           else
+             error ("Unknown parameter: " ^ quote 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 " "