diff -r a973f82fc885 -r 87389311ba78 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu May 12 23:23:48 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri May 13 10:10:43 2011 +0200
@@ -120,10 +120,16 @@
     ss as _ :: _ => forall (is_prover_supported ctxt) ss
   | _ => false
 
+(* Secret feature: "provers =" and "type_sys =" can be left out. *)
 fun check_and_repair_raw_param ctxt (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 error ("Unknown parameter: " ^ quote name ^ ".")
+  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_sys_from_string name andalso null value then
+    ("type_sys", [name])
+  else
+    error ("Unknown parameter: " ^ quote name ^ ".")
 
 fun unalias_raw_param (name, value) =
   case AList.lookup (op =) alias_params name of
@@ -170,9 +176,9 @@
 
 (* Ensure that type systems such as "simple!" and "mangled_preds?" are handled
    correctly. *)
-fun implode_param_value [s, "?"] = s ^ "?"
-  | implode_param_value [s, "!"] = s ^ "!"
-  | implode_param_value ss = space_implode " " ss
+fun implode_param [s, "?"] = s ^ "?"
+  | implode_param [s, "!"] = s ^ "!"
+  | implode_param ss = space_implode " " ss
 
 (* The first ATP of the list is used by Auto Sledgehammer. Because of the low
    timeout, it makes sense to put SPASS first. *)
@@ -180,7 +186,7 @@
   [spassN, eN, vampireN, sine_eN, SMT_Solver.solver_name_of ctxt]
   |> map_filter (remotify_prover_if_not_installed ctxt)
   |> avoid_too_many_local_threads ctxt (Multithreading.max_threads_value ())
-  |> implode_param_value
+  |> implode_param
 
 val set_default_raw_param = Data.map o AList.update (op =) o unalias_raw_param
 fun default_raw_params ctxt =
@@ -204,7 +210,7 @@
   let
     val override_params = map unalias_raw_param override_params
     val raw_params = rev override_params @ rev default_params
-    val lookup = Option.map implode_param_value o AList.lookup (op =) raw_params
+    val lookup = Option.map implode_param o AList.lookup (op =) raw_params
     val lookup_string = the_default "" o lookup
     fun general_lookup_bool option default_value name =
       case lookup name of
@@ -285,7 +291,7 @@
 val is_raw_param_relevant_for_minimize =
   member (op =) params_for_minimize o fst o unalias_raw_param
 fun string_for_raw_param (key, values) =
-  key ^ (case implode_param_value values of "" => "" | value => " = " ^ value)
+  key ^ (case implode_param values of "" => "" | value => " = " ^ value)
 
 fun minimize_command override_params i prover_name fact_names =
   sledgehammerN ^ " " ^ minimizeN ^ " [prover = " ^ prover_name ^
@@ -328,7 +334,7 @@
   Toplevel.keep (hammer_away params subcommand opt_i relevance_override
                  o Toplevel.proof_of)
 
-fun string_for_raw_param (name, value) = name ^ " = " ^ implode_param_value value
+fun string_for_raw_param (name, value) = name ^ " = " ^ implode_param value
 
 fun sledgehammer_params_trans params =
   Toplevel.theory
@@ -344,7 +350,9 @@
                                        |> sort_strings |> cat_lines))
                   end))
 
-val parse_key = Scan.repeat1 Parse.typ_group >> space_implode " "
+val parse_key =
+  Scan.repeat1 (Parse.typ_group || Parse.$$$ "?" || Parse.$$$ "!")
+               >> implode_param
 val parse_value =
   Scan.repeat1 (Parse.xname || Parse.float_number || Parse.$$$ "?"
                 || Parse.$$$ "!")