# HG changeset patch
# User blanchet
# Date 1292675894 -3600
# Node ID b6b77c963f11b6bd063e976dfeab08e4db041a7d
# Parent  a393d6d8e198ad6a9985bcd2a68091f69379a48f
compile

diff -r a393d6d8e198 -r b6b77c963f11 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Sat Dec 18 13:34:32 2010 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Sat Dec 18 13:38:14 2010 +0100
@@ -468,7 +468,7 @@
        ("type_sys", type_sys),
        ("timeout", Int.toString timeout)]
     val minimize =
-      Sledgehammer_Minimize.minimize_facts params true 1
+      Sledgehammer_Minimize.minimize_facts prover_name params true 1
                                            (Sledgehammer_Util.subgoal_count st)
     val _ = log separator
   in