# HG changeset patch
# User blanchet
# Date 1272466563 -7200
# Node ID 7ec5ceef117b151348f173b68431f90ebb317e06
# Parent  c36bbcb006893c401896ff09e459242cda795445
make Mirabelle happy

diff -r c36bbcb00689 -r 7ec5ceef117b src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Wed Apr 28 16:47:56 2010 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Wed Apr 28 16:56:03 2010 +0200
@@ -377,6 +377,8 @@
 end
 
 
+val subgoal_count = Logic.count_prems o prop_of o #goal o Proof.goal
+
 fun run_minimize args named_thms id ({pre=st, log, ...}: Mirabelle.run_args) =
   let
     open Sledgehammer_Fact_Minimizer
@@ -390,7 +392,7 @@
       |> the_default 5
     val params = default_params thy
       [("atps", prover_name), ("minimize_timeout", Int.toString timeout)]
-    val minimize = minimize_theorems params 1
+    val minimize = minimize_theorems params 1 (subgoal_count st)
     val _ = log separator
   in
     case minimize st (these (!named_thms)) of