# HG changeset patch
# User blanchet
# Date 1357918256 -3600
# Node ID 01c9a515ccdd246a5d7a8a89d6f23dbf1dca7a5e
# Parent  91e6836bb68bf9f79ef311212a78b34b483e4d48
fixed escaping for MeSh encoder

diff -r 91e6836bb68b -r 01c9a515ccdd src/HOL/TPTP/mash_export.ML
--- a/src/HOL/TPTP/mash_export.ML	Fri Jan 11 16:30:56 2013 +0100
+++ b/src/HOL/TPTP/mash_export.ML	Fri Jan 11 16:30:56 2013 +0100
@@ -203,19 +203,18 @@
     val _ = File.write mesh_path ""
     fun do_fact (mash_line, mepo_line) =
       let
-        val (mash_name, mash_suggs) =
+        val (name, mash_suggs) =
           extract_suggestions mash_line
           ||> (map fst #> weight_mash_facts)
-        val (mepo_name, mepo_suggs) =
+        val (name', mepo_suggs) =
           extract_suggestions mepo_line
           ||> (map fst #> weight_mash_facts)
-        val _ =
-          if mash_name = mepo_name then () else error "Input files out of sync."
+        val _ = if name = name' then () else error "Input files out of sync."
         val mess =
           [(mepo_weight, (mepo_suggs, [])),
            (mash_weight, (mash_suggs, []))]
         val mesh_suggs = mesh_facts (op =) max_suggs mess
-        val mesh_line = mash_name ^ ": " ^ space_implode " " mesh_suggs ^ "\n"
+        val mesh_line = encode_str name ^ ": " ^ encode_strs mesh_suggs ^ "\n"
       in File.append mesh_path mesh_line end
     val mash_lines = Path.explode mash_file_name |> File.read_lines
     val mepo_lines = Path.explode mepo_file_name |> File.read_lines