Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
escape nicknames
authorblanchet
Sun, 16 Dec 2012 14:19:08 +0100
changeset 50563 3a4785d64ecb
parent 50562 0a7c7e121bd8
child 50564 c6fde2fc4217
child 50567 768a3fbe4149
escape nicknames
src/HOL/TPTP/mash_eval.ML file | annotate | diff | comparison | revisions 
--- 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)
isabelle