# HG changeset patch
# User blanchet
# Date 1355656076 -3600
# Node ID 0a7c7e121bd85b24873ac9e623b68f64a087f027
# Parent  9a733bd6c0ba0b155cdf394f84b041e86d942426
generate proper nicks also for instantiated induction rules

diff -r 9a733bd6c0ba -r 0a7c7e121bd8 src/HOL/TPTP/mash_eval.ML
--- a/src/HOL/TPTP/mash_eval.ML	Sun Dec 16 12:07:37 2012 +0100
+++ b/src/HOL/TPTP/mash_eval.ML	Sun Dec 16 12:07:56 2012 +0100
@@ -114,10 +114,9 @@
                 ((K (nickname_of th), stature), th)
               val facts =
                 facts
-                |> map get
+                |> map (get #> nickify)
                 |> 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