escape nicknames
authorblanchet
Sun Dec 16 14:19:08 2012 +0100 (2012-12-16)
changeset 505633a4785d64ecb
parent 50562 0a7c7e121bd8
child 50564 c6fde2fc4217
child 50567 768a3fbe4149
escape nicknames
src/HOL/TPTP/mash_eval.ML
     1.1 --- a/src/HOL/TPTP/mash_eval.ML	Sun Dec 16 12:07:56 2012 +0100
     1.2 +++ b/src/HOL/TPTP/mash_eval.ML	Sun Dec 16 14:19:08 2012 +0100
     1.3 @@ -111,7 +111,7 @@
     1.4            fun prove ok heading get facts =
     1.5              let
     1.6                fun nickify ((_, stature), th) =
     1.7 -                ((K (nickname_of th), stature), th)
     1.8 +                ((K (escape_meta (nickname_of th)), stature), th)
     1.9                val facts =
    1.10                  facts
    1.11                  |> map (get #> nickify)