--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri May 27 10:30:07 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri May 27 10:30:08 2011 +0200
@@ -312,7 +312,7 @@
key ^ (case implode_param values of "" => "" | value => " = " ^ value)
fun minimize_command override_params i prover_name fact_names =
- sledgehammerN ^ " " ^ minN ^ " [prover = " ^ prover_name ^
+ sledgehammerN ^ " " ^ minN ^ " [" ^ prover_name ^
(override_params |> filter is_raw_param_relevant_for_minimize
|> implode o map (prefix ", " o string_for_raw_param)) ^
"] (" ^ space_implode " " fact_names ^ ")" ^