src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
changeset 41338 ffd730fcf0ac
parent 41337 263fe1670067
child 41357 ae76960d86a2
--- 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