--- 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