1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu May 12 23:23:48 2011 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri May 13 10:10:43 2011 +0200
     1.3 @@ -120,10 +120,16 @@
     1.4      ss as _ :: _ => forall (is_prover_supported ctxt) ss
     1.5    | _ => false
     1.6  
     1.7 +(* Secret feature: "provers =" and "type_sys =" can be left out. *)
     1.8  fun check_and_repair_raw_param ctxt (name, value) =
     1.9 -  if is_known_raw_param name then (name, value)
    1.10 -  else if is_prover_list ctxt name andalso null value then ("provers", [name])
    1.11 -  else error ("Unknown parameter: " ^ quote name ^ ".")
    1.12 +  if is_known_raw_param name then
    1.13 +    (name, value)
    1.14 +  else if is_prover_list ctxt name andalso null value then
    1.15 +    ("provers", [name])
    1.16 +  else if can type_sys_from_string name andalso null value then
    1.17 +    ("type_sys", [name])
    1.18 +  else
    1.19 +    error ("Unknown parameter: " ^ quote name ^ ".")
    1.20  
    1.21  fun unalias_raw_param (name, value) =
    1.22    case AList.lookup (op =) alias_params name of
    1.23 @@ -170,9 +176,9 @@
    1.24  
    1.25  (* Ensure that type systems such as "simple!" and "mangled_preds?" are handled
    1.26     correctly. *)
    1.27 -fun implode_param_value [s, "?"] = s ^ "?"
    1.28 -  | implode_param_value [s, "!"] = s ^ "!"
    1.29 -  | implode_param_value ss = space_implode " " ss
    1.30 +fun implode_param [s, "?"] = s ^ "?"
    1.31 +  | implode_param [s, "!"] = s ^ "!"
    1.32 +  | implode_param ss = space_implode " " ss
    1.33  
    1.34  (* The first ATP of the list is used by Auto Sledgehammer. Because of the low
    1.35     timeout, it makes sense to put SPASS first. *)
    1.36 @@ -180,7 +186,7 @@
    1.37    [spassN, eN, vampireN, sine_eN, SMT_Solver.solver_name_of ctxt]
    1.38    |> map_filter (remotify_prover_if_not_installed ctxt)
    1.39    |> avoid_too_many_local_threads ctxt (Multithreading.max_threads_value ())
    1.40 -  |> implode_param_value
    1.41 +  |> implode_param
    1.42  
    1.43  val set_default_raw_param = Data.map o AList.update (op =) o unalias_raw_param
    1.44  fun default_raw_params ctxt =
    1.45 @@ -204,7 +210,7 @@
    1.46    let
    1.47      val override_params = map unalias_raw_param override_params
    1.48      val raw_params = rev override_params @ rev default_params
    1.49 -    val lookup = Option.map implode_param_value o AList.lookup (op =) raw_params
    1.50 +    val lookup = Option.map implode_param o AList.lookup (op =) raw_params
    1.51      val lookup_string = the_default "" o lookup
    1.52      fun general_lookup_bool option default_value name =
    1.53        case lookup name of
    1.54 @@ -285,7 +291,7 @@
    1.55  val is_raw_param_relevant_for_minimize =
    1.56    member (op =) params_for_minimize o fst o unalias_raw_param
    1.57  fun string_for_raw_param (key, values) =
    1.58 -  key ^ (case implode_param_value values of "" => "" | value => " = " ^ value)
    1.59 +  key ^ (case implode_param values of "" => "" | value => " = " ^ value)
    1.60  
    1.61  fun minimize_command override_params i prover_name fact_names =
    1.62    sledgehammerN ^ " " ^ minimizeN ^ " [prover = " ^ prover_name ^
    1.63 @@ -328,7 +334,7 @@
    1.64    Toplevel.keep (hammer_away params subcommand opt_i relevance_override
    1.65                   o Toplevel.proof_of)
    1.66  
    1.67 -fun string_for_raw_param (name, value) = name ^ " = " ^ implode_param_value value
    1.68 +fun string_for_raw_param (name, value) = name ^ " = " ^ implode_param value
    1.69  
    1.70  fun sledgehammer_params_trans params =
    1.71    Toplevel.theory
    1.72 @@ -344,7 +350,9 @@
    1.73                                         |> sort_strings |> cat_lines))
    1.74                    end))
    1.75  
    1.76 -val parse_key = Scan.repeat1 Parse.typ_group >> space_implode " "
    1.77 +val parse_key =
    1.78 +  Scan.repeat1 (Parse.typ_group || Parse.$$$ "?" || Parse.$$$ "!")
    1.79 +               >> implode_param
    1.80  val parse_value =
    1.81    Scan.repeat1 (Parse.xname || Parse.float_number || Parse.$$$ "?"
    1.82                  || Parse.$$$ "!")