--- a/src/HOL/TPTP/mash_eval.ML Mon Dec 10 13:02:56 2012 +0100
+++ b/src/HOL/TPTP/mash_eval.ML Mon Dec 10 13:33:06 2012 +0100
@@ -21,7 +21,7 @@
val MePoN = "MePo"
val MaShN = "MaSh"
-val MeshN = "Mesh"
+val MeShN = "MeSh"
val IsarN = "Isar"
val all_names = map (rpair () o nickname_of) #> Symtab.make
@@ -112,7 +112,7 @@
val [mepo_s, mash_s, mesh_s, isar_s] =
[fn () => prove mepo_ok MePoN fst mepo_facts,
fn () => prove mash_ok MaShN fst mash_facts,
- fn () => prove mesh_ok MeshN I mesh_facts,
+ fn () => prove mesh_ok MeShN I mesh_facts,
fn () => prove isar_ok IsarN fst isar_facts]
|> (* Par_List. *) map (fn f => f ())
in
@@ -138,7 +138,7 @@
["Successes (of " ^ string_of_int n ^ " goals)",
total_of MePoN mepo_ok n,
total_of MaShN mash_ok n,
- total_of MeshN mesh_ok n,
+ total_of MeShN mesh_ok n,
total_of IsarN isar_ok n]
|> cat_lines |> print
end