src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
changeset 32598 3a3d2e37fec4
parent 32585 e788b33dd2b4
child 32607 e7fe01b74a92
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Wed Sep 16 13:03:03 2009 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu Sep 17 19:13:07 2009 +0200
@@ -192,8 +192,6 @@
  (log ("Total number of " ^ tag ^ "metis calls: " ^ str metis_calls);
   log ("Number of successful " ^ tag ^ "metis calls: " ^ str metis_success);
   log ("Number of " ^ tag ^ "metis timeouts: " ^ str metis_timeout);
-  log ("Number of " ^ tag ^ "metis exceptions: " ^
-    str (sh_success - metis_success - metis_timeout));
   log ("Success rate: " ^ percentage metis_success sh_calls ^ "%");
   log ("Number of successful " ^ tag ^ "metis lemmas: " ^ str metis_lemmas);
   log ("Total time for successful metis calls: " ^ str3 (time metis_time));