# HG changeset patch
# User blanchet
# Date 1355593738 -3600
# Node ID 6209bc89faa36818bb4f55b83433651f506873ec
# Parent  81a1491ba936967aaa9a29565540ad0e1ba65ba5
proper escaping in file name

diff -r 81a1491ba936 -r 6209bc89faa3 src/HOL/TPTP/mash_eval.ML
--- a/src/HOL/TPTP/mash_eval.ML	Sat Dec 15 18:26:37 2012 +0100
+++ b/src/HOL/TPTP/mash_eval.ML	Sat Dec 15 18:48:58 2012 +0100
@@ -90,7 +90,8 @@
         fun set_file_name heading (SOME dir) =
             let
               val prob_prefix =
-                "goal_" ^ string_of_int j ^ "__" ^ name ^ "__" ^ heading
+                "goal_" ^ string_of_int j ^ "__" ^ escape_meta name ^ "__" ^
+                heading
             in
               Config.put Sledgehammer_Provers.dest_dir dir
               #> Config.put Sledgehammer_Provers.problem_prefix