--- 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 " "