# HG changeset patch
# User nipkow
# Date 1252305142 -7200
# Node ID e6996fb0a774c322e81d33940e1f82dbc6c46c34
# Parent  ea322e847633bef68360a88c990690cdd39d491a
enabled metis permanently, tuned stats

diff -r ea322e847633 -r e6996fb0a774 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- 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