# HG changeset patch
# User blanchet
# Date 1292910800 -3600
# Node ID ffd730fcf0ac04c141c9e2ac7db6cecf8d514eda
# Parent  263fe1670067d49d5ec49c993d06170f847e30b4
avoid weird symbols in path

diff -r 263fe1670067 -r ffd730fcf0ac src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue Dec 21 06:06:28 2010 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue Dec 21 06:53:20 2010 +0100
@@ -350,7 +350,8 @@
     fun change_dir (SOME dir) =
         Config.put Sledgehammer_Provers.dest_dir dir
         #> Config.put SMT_Config.debug_files
-          (dir ^ "/" ^ ATP_Problem.timestamp () ^ "_" ^ serial_string ())
+          (dir ^ "/" ^ Name.desymbolize false (ATP_Problem.timestamp ()) ^ "_"
+          ^ serial_string ())
       | change_dir NONE = I
     val st' =
       st |> Proof.map_context