# 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