1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Nov 16 13:22:36 2011 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Nov 16 16:35:19 2011 +0100
     1.3 @@ -282,7 +282,7 @@
     1.4          "smart" => NONE
     1.5        | s => (type_enc_from_string Sound s; SOME s)
     1.6      val sound = mode = Auto_Try orelse lookup_bool "sound"
     1.7 -    val lam_trans = lookup_string "lam_trans"
     1.8 +    val lam_trans = lookup_option lookup_string "lam_trans"
     1.9      val relevance_thresholds = lookup_real_pair "relevance_thresholds"
    1.10      val max_relevant = lookup_option lookup_int "max_relevant"
    1.11      val max_mono_iters = lookup_int "max_mono_iters"
    1.12 @@ -318,10 +318,13 @@
    1.13  fun string_for_raw_param (key, values) =
    1.14    key ^ (case implode_param values of "" => "" | value => " = " ^ value)
    1.15  
    1.16 -fun minimize_command override_params i prover_name fact_names =
    1.17 +fun minimize_command override_params i more_override_params prover_name
    1.18 +                     fact_names =
    1.19    let
    1.20      val params =
    1.21 -      override_params
    1.22 +      (override_params
    1.23 +       |> filter_out (AList.defined (op =) more_override_params o fst)) @
    1.24 +      more_override_params
    1.25        |> filter is_raw_param_relevant_for_minimize
    1.26        |> map string_for_raw_param
    1.27        |> (if prover_name = default_minimize_prover then I else cons prover_name)