# HG changeset patch
# User nipkow
# Date 1253207602 -7200
# Node ID 979c274089a504c09ab42e3afa03000721c2c641
# Parent  1e2872252f913ef37281435a82cb2fdcf2128d50# Parent  3a3d2e37fec495123fd3405d130946f7276c50f5
merged

diff -r 1e2872252f91 -r 979c274089a5 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu Sep 17 15:04:46 2009 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu Sep 17 19:13:22 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));