diff -r 9f77084444df -r ee65e9cfe284 src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML	Thu Aug 28 16:58:27 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML	Thu Aug 28 16:58:27 2014 +0200
@@ -191,7 +191,7 @@
     facts =
   let
     val ctxt = Proof.context_of state
-    val prover = get_prover ctxt (if silent then Auto_Minimize else Minimize) prover_name
+    val prover = get_prover ctxt Minimize prover_name
     fun test timeout = test_facts params silent prover timeout i n state goal
     val (chained, non_chained) = List.partition is_fact_chained facts
     (* Push chained facts to the back, so that they are less likely to be kicked out by the linear