1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Sep 05 14:17:44 2011 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Sep 05 14:42:31 2011 +0200
     1.3 @@ -124,18 +124,6 @@
     1.4      ss as _ :: _ => forall (is_prover_supported ctxt) ss
     1.5    | _ => false
     1.6  
     1.7 -(* "provers =" and "type_enc =" can be left out. The latter is a secret
     1.8 -   feature. *)
     1.9 -fun check_and_repair_raw_param ctxt (name, value) =
    1.10 -  if is_known_raw_param name then
    1.11 -    (name, value)
    1.12 -  else if is_prover_list ctxt name andalso null value then
    1.13 -    ("provers", [name])
    1.14 -  else if can (type_enc_from_string Sound) name andalso null value then
    1.15 -    ("type_enc", [name])
    1.16 -  else
    1.17 -    error ("Unknown parameter: " ^ quote name ^ ".")
    1.18 -
    1.19  fun unalias_raw_param (name, value) =
    1.20    case AList.lookup (op =) alias_params name of
    1.21      SOME name' => (name', value)
    1.22 @@ -148,6 +136,21 @@
    1.23                              | _ => value)
    1.24      | NONE => (name, value)
    1.25  
    1.26 +(* "provers =" and "type_enc =" can be left out. The latter is a secret
    1.27 +   feature. *)
    1.28 +fun normalize_raw_param ctxt =
    1.29 +  unalias_raw_param
    1.30 +  #> (fn (name, value) =>
    1.31 +         if is_known_raw_param name then
    1.32 +           (name, value)
    1.33 +         else if is_prover_list ctxt name andalso null value then
    1.34 +           ("provers", [name])
    1.35 +         else if can (type_enc_from_string Sound) name andalso null value then
    1.36 +           ("type_enc", [name])
    1.37 +         else
    1.38 +           error ("Unknown parameter: " ^ quote name ^ "."))
    1.39 +
    1.40 +
    1.41  (* Ensure that type systems such as "mono_simple!" and "mono_guards?" are
    1.42     handled correctly. *)
    1.43  fun implode_param [s, "?"] = s ^ "?"
    1.44 @@ -205,7 +208,10 @@
    1.45                                    max_default_remote_threads)
    1.46    |> implode_param
    1.47  
    1.48 -val set_default_raw_param = Data.map o AList.update (op =) o unalias_raw_param
    1.49 +fun set_default_raw_param param thy =
    1.50 +  let val ctxt = Proof_Context.init_global thy in
    1.51 +    thy |> Data.map (AList.update (op =) (normalize_raw_param ctxt param))
    1.52 +  end
    1.53  fun default_raw_params ctxt =
    1.54    let val thy = Proof_Context.theory_of ctxt in
    1.55      Data.get thy
    1.56 @@ -224,7 +230,6 @@
    1.57  
    1.58  fun extract_params mode default_params override_params =
    1.59    let
    1.60 -    val override_params = map unalias_raw_param override_params
    1.61      val raw_params = rev override_params @ rev default_params
    1.62      val lookup = Option.map implode_param o AList.lookup (op =) raw_params
    1.63      val lookup_string = the_default "" o lookup
    1.64 @@ -294,15 +299,15 @@
    1.65       timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}
    1.66    end
    1.67  
    1.68 -fun get_params mode ctxt = extract_params mode (default_raw_params ctxt)
    1.69 +fun get_params mode = extract_params mode o default_raw_params
    1.70  fun default_params thy = get_params Normal thy o map (apsnd single)
    1.71  
    1.72  (* Sledgehammer the given subgoal *)
    1.73  
    1.74  val default_minimize_prover = Metis_Tactic.metisN
    1.75  
    1.76 -val is_raw_param_relevant_for_minimize =
    1.77 -  member (op =) params_for_minimize o fst o unalias_raw_param
    1.78 +fun is_raw_param_relevant_for_minimize (name, _) =
    1.79 +  member (op =) params_for_minimize name
    1.80  fun string_for_raw_param (key, values) =
    1.81    key ^ (case implode_param values of "" => "" | value => " = " ^ value)
    1.82  
    1.83 @@ -324,8 +329,7 @@
    1.84  fun hammer_away override_params subcommand opt_i relevance_override state =
    1.85    let
    1.86      val ctxt = Proof.context_of state
    1.87 -    val override_params =
    1.88 -      override_params |> map (check_and_repair_raw_param ctxt)
    1.89 +    val override_params = override_params |> map (normalize_raw_param ctxt)
    1.90    in
    1.91      if subcommand = runN then
    1.92        let val i = the_default 1 opt_i in
    1.93 @@ -368,8 +372,7 @@
    1.94                               (case default_raw_params ctxt |> rev of
    1.95                                  [] => "none"
    1.96                                | params =>
    1.97 -                                params |> map (check_and_repair_raw_param ctxt)
    1.98 -                                       |> map string_for_raw_param
    1.99 +                                params |> map string_for_raw_param
   1.100                                         |> sort_strings |> cat_lines))
   1.101                    end))
   1.102