# HG changeset patch
# User blanchet
# Date 1360242333 -3600
# Node ID 7327a847f0c73b9e58f664b179499f9bb905e522
# Parent  0f817f80bcca7b27acf4b63a6bce6ebcda57c47e
more robustness w.r.t. 0

diff -r 0f817f80bcca -r 7327a847f0c7 src/HOL/TPTP/mash_eval.ML
--- a/src/HOL/TPTP/mash_eval.ML	Thu Feb 07 14:05:33 2013 +0100
+++ b/src/HOL/TPTP/mash_eval.ML	Thu Feb 07 14:05:33 2013 +0100
@@ -43,6 +43,7 @@
         mepo_file_name mash_isar_file_name mash_prover_file_name
         mesh_isar_file_name mesh_prover_file_name report_file_name =
   let
+    val zeros = [0, 0, 0, 0, 0, 0]
     val report_path = report_file_name |> Path.explode
     val _ = File.write report_path ""
     fun print s = File.append report_path (s ^ "\n")
@@ -180,11 +181,11 @@
           map snd ress
         end
       else
-        [0, 0, 0, 0, 0, 0]
+        zeros
     fun total_of method ok n =
       str_of_method method ^ string_of_int ok ^ " (" ^
       Real.fmt (StringCvt.FIX (SOME 1))
-               (100.0 * Real.fromInt ok / Real.fromInt n) ^ "%)"
+               (100.0 * Real.fromInt ok / Real.fromInt (Int.max (1, n))) ^ "%)"
     val inst_inducts = Config.get ctxt instantiate_inducts
     val options =
       ["prover = " ^ prover,
@@ -200,7 +201,7 @@
     val n = length oks
     val [mepo_ok, mash_isar_ok, mash_prover_ok, mesh_isar_ok, mesh_prover_ok,
          isar_ok] =
-      map Integer.sum (map_transpose I oks)
+      if n = 0 then zeros else map Integer.sum (map_transpose I oks)
   in
     ["Successes (of " ^ string_of_int n ^ " goals)",
      total_of MePoN mepo_ok n,