1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Fri Nov 18 11:47:12 2011 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Fri Nov 18 11:47:12 2011 +0100
     1.3 @@ -172,7 +172,8 @@
     1.4                     facts =
     1.5    let
     1.6      val ctxt = Proof.context_of state
     1.7 -    val prover = get_prover ctxt Minimize prover_name
     1.8 +    val prover =
     1.9 +      get_prover ctxt (if silent then Auto_Minimize else Minimize) prover_name
    1.10      val _ = print silent (fn () => "Sledgehammer minimizer: " ^
    1.11                                     quote prover_name ^ ".")
    1.12      fun test timeout = test_facts params silent prover timeout i n state