# HG changeset patch
# User blanchet
# Date 1277715842 -7200
# Node ID 466031e057a0f8e1df1eb9ee276410ccde5c48a5
# Parent  a209fff747920764f3ebff21d1fc24b481b50d93
compile

diff -r a209fff74792 -r 466031e057a0 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Mon Jun 28 08:55:46 2010 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Mon Jun 28 11:04:02 2010 +0200
@@ -393,7 +393,8 @@
       |> the_default 5
     val params = default_params thy
       [("atps", prover_name), ("minimize_timeout", Int.toString timeout)]
-    val minimize = minimize_theorems params 1 (subgoal_count st)
+    val minimize =
+      Sledgehammer_Fact_Minimizer.minimize_theorems params 1 (subgoal_count st)
     val _ = log separator
   in
     case minimize st (these (!named_thms)) of