src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
changeset 43057 884b0bc19de4
parent 43051 d7075adac3bd
child 43064 b6e61d22fa61
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon May 30 17:00:38 2011 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon May 30 17:00:38 2011 +0200
     1.3 @@ -317,13 +317,19 @@
     1.4    key ^ (case implode_param values of "" => "" | value => " = " ^ value)
     1.5  
     1.6  fun minimize_command override_params i prover_name fact_names =
     1.7 -  sledgehammerN ^ " " ^ minN ^
     1.8 -  (if prover_name = default_minimize_prover then ""
     1.9 -   else enclose "[" "]" prover_name) ^
    1.10 -  (override_params |> filter is_raw_param_relevant_for_minimize
    1.11 -                   |> implode o map (prefix ", " o string_for_raw_param)) ^
    1.12 -  " (" ^ space_implode " " fact_names ^ ")" ^
    1.13 -  (if i = 1 then "" else " " ^ string_of_int i)
    1.14 +  let
    1.15 +    val params =
    1.16 +      override_params
    1.17 +      |> filter is_raw_param_relevant_for_minimize
    1.18 +      |> map string_for_raw_param
    1.19 +      |> (if prover_name = default_minimize_prover then I else cons prover_name)
    1.20 +      |> space_implode ", "
    1.21 +  in
    1.22 +    sledgehammerN ^ " " ^ minN ^
    1.23 +    (if params = "" then "" else enclose " [" "]" params) ^
    1.24 +    " (" ^ space_implode " " fact_names ^ ")" ^
    1.25 +    (if i = 1 then "" else " " ^ string_of_int i)
    1.26 +  end
    1.27  
    1.28  fun hammer_away override_params subcommand opt_i relevance_override state =
    1.29    let