# HG changeset patch
# User blanchet
# Date 1306485008 -7200
# Node ID 3a95b1ae796d5afab132a4c30ff0bf04954c26ab
# Parent  c01c3007e07bcf46c00e70ddf4b74836a74f3637
shorten minimizer command further, exploiting until-now-undocumented syntax

diff -r c01c3007e07b -r 3a95b1ae796d src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- 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 ^ ")" ^