# HG changeset patch
# User nipkow
# Date 1253207587 -7200
# Node ID 3a3d2e37fec495123fd3405d130946f7276c50f5
# Parent  db1afe8ee3d72c21aa21afe1119482e8be992c4e
removed misleading log line

diff -r db1afe8ee3d7 -r 3a3d2e37fec4 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- 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));