--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Sat Sep 05 22:01:31 2009 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Mon Sep 07 08:32:22 2009 +0200
@@ -97,7 +97,7 @@
log ("Number of metis timeouts: " ^ str metis_timeout);
log ("Number of metis exceptions: " ^
str (sh_success - metis_success - metis_timeout));
- log ("Success rate: " ^ percentage metis_success metis_calls ^ "%");
+ log ("Success rate: " ^ percentage metis_success sh_success ^ "%");
log ("Total time for successful metis calls: " ^ str3 (time metis_time));
log ("Average time for successful metis calls: " ^
str3 (avg_time metis_time metis_success)))
@@ -266,6 +266,7 @@
fun invoke args =
let
+ val args = (metisK,"yes") :: args; (* always enable metis *)
val _ = AtpManager.set_full_types (AList.defined (op =) args full_typesK)
in Mirabelle.register (init, sledgehammer_action args, done) end