# HG changeset patch
# User blanchet
# Date 1355663948 -3600
# Node ID 3a4785d64ecbb8347312eebfa497da0a7829b646
# Parent  0a7c7e121bd85b24873ac9e623b68f64a087f027
escape nicknames

diff -r 0a7c7e121bd8 -r 3a4785d64ecb src/HOL/TPTP/mash_eval.ML
--- a/src/HOL/TPTP/mash_eval.ML	Sun Dec 16 12:07:56 2012 +0100
+++ b/src/HOL/TPTP/mash_eval.ML	Sun Dec 16 14:19:08 2012 +0100
@@ -111,7 +111,7 @@
           fun prove ok heading get facts =
             let
               fun nickify ((_, stature), th) =
-                ((K (nickname_of th), stature), th)
+                ((K (escape_meta (nickname_of th)), stature), th)
               val facts =
                 facts
                 |> map (get #> nickify)