--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri May 27 10:30:08 2011 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Fri May 27 10:30:08 2011 +0200
@@ -327,7 +327,8 @@
hd (#provers (Sledgehammer_Isar.default_params ctxt []))
handle Empty => error "No ATP available."
fun get_prover name =
- (name, Sledgehammer_Run.get_minimizing_prover ctxt false name)
+ (name, Sledgehammer_Run.get_minimizing_prover ctxt
+ Sledgehammer_Provers.Normal name)
in
(case AList.lookup (op =) args proverK of
SOME name => get_prover name