author | blanchet |
Sat, 18 Dec 2010 13:38:14 +0100 | |
changeset 41266 | b6b77c963f11 |
parent 41265 | a393d6d8e198 |
child 41267 | 958fee9ec275 |
--- 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