# HG changeset patch
# User blanchet
# Date 1355435347 -3600
# Node ID f2d33310337a471a41de05672e1f95961c4deac3
# Parent  2951841ec0110031bd12c61259330b47e968230c
use MaSh nicknames in ATP problem files to facilitate gathering of statistics

diff -r 2951841ec011 -r f2d33310337a src/HOL/TPTP/mash_eval.ML
--- a/src/HOL/TPTP/mash_eval.ML	Thu Dec 13 22:49:06 2012 +0100
+++ b/src/HOL/TPTP/mash_eval.ML	Thu Dec 13 22:49:07 2012 +0100
@@ -97,11 +97,13 @@
           | set_file_name _ NONE = I
         fun prove ok heading get facts =
           let
+            fun nickify ((_, stature), th) = ((K (nickname_of th), stature), th)
             val facts =
-              facts |> map get
-                    |> Sledgehammer_Fact.maybe_instantiate_inducts ctxt hyp_ts
-                                                                   concl_t
-                    |> take (the max_facts)
+              facts
+              |> map get
+              |> Sledgehammer_Fact.maybe_instantiate_inducts ctxt hyp_ts concl_t
+              |> take (the max_facts)
+              |> map nickify
             val ctxt = ctxt |> set_file_name heading prob_dir_name
             val res as {outcome, ...} =
               run_prover_for_mash ctxt params prover facts goal