# HG changeset patch
# User blanchet
# Date 1356600081 -3600
# Node ID 07e08250a8803aac685344fcade47b98ffe1f7c7
# Parent  b958a94cf8110458bde3bb0f758a2eec6ff91a24
fixed total

diff -r b958a94cf811 -r 07e08250a880 src/HOL/TPTP/mash_eval.ML
--- a/src/HOL/TPTP/mash_eval.ML	Thu Dec 27 10:01:40 2012 +0100
+++ b/src/HOL/TPTP/mash_eval.ML	Thu Dec 27 10:21:21 2012 +0100
@@ -145,7 +145,7 @@
     val _ = print " * * *";
     val _ = print ("Options: " ^ commas options);
     val oks = Par_List.map solve_goal (tag_list 1 lines)
-    val n = length (hd oks)
+    val n = length oks
     val [mepo_ok, mash_ok, mesh_ok, isar_ok] =
       map Integer.sum (map_transpose I oks)
   in