--- 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