changeset 41266 | b6b77c963f11 |
parent 41264 | a96b0b62f588 |
child 41268 | 56b7e277fd7d |
--- 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