--- 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