# HG changeset patch
# User blanchet
# Date 1292673333 -3600
# Node ID a96b0b62f5880e36b868b9a8ecec9ae309c508bf
# Parent  4cac389c005faafe781dea84fe6f2068315cb1f8
use minimizing prover in Mirabelle

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