diff -r 4cac389c005f -r a96b0b62f588 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Sat Dec 18 12:53:56 2010 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Sat Dec 18 12:55:33 2010 +0100
@@ -321,7 +321,7 @@
       hd (#provers (Sledgehammer_Isar.default_params ctxt []))
       handle Empty => error "No ATP available."
     fun get_prover name =
-      (name, Sledgehammer_Provers.get_prover ctxt false name)
+      (name, Sledgehammer_Run.get_minimizing_prover ctxt false name)
   in
     (case AList.lookup (op =) args proverK of
       SOME name => get_prover name