# HG changeset patch
# User blanchet
# Date 1306767638 -7200
# Node ID 884b0bc19de404b580991582a2824972a0c87f8b
# Parent  7a43449ffd861b9a402855105c6a7e2c01971a63
fixed syntax of min options

diff -r 7a43449ffd86 -r 884b0bc19de4 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon May 30 17:00:38 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon May 30 17:00:38 2011 +0200
@@ -317,13 +317,19 @@
   key ^ (case implode_param values of "" => "" | value => " = " ^ value)
 
 fun minimize_command override_params i prover_name fact_names =
-  sledgehammerN ^ " " ^ minN ^
-  (if prover_name = default_minimize_prover then ""
-   else enclose "[" "]" prover_name) ^
-  (override_params |> filter is_raw_param_relevant_for_minimize
-                   |> implode o map (prefix ", " o string_for_raw_param)) ^
-  " (" ^ space_implode " " fact_names ^ ")" ^
-  (if i = 1 then "" else " " ^ string_of_int i)
+  let
+    val params =
+      override_params
+      |> filter is_raw_param_relevant_for_minimize
+      |> map string_for_raw_param
+      |> (if prover_name = default_minimize_prover then I else cons prover_name)
+      |> space_implode ", "
+  in
+    sledgehammerN ^ " " ^ minN ^
+    (if params = "" then "" else enclose " [" "]" params) ^
+    " (" ^ space_implode " " fact_names ^ ")" ^
+    (if i = 1 then "" else " " ^ string_of_int i)
+  end
 
 fun hammer_away override_params subcommand opt_i relevance_override state =
   let