mechanism to keep SMT input and output files around in Mirabelle

--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue Dec 21 04:33:17 2010 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue Dec 21 06:06:28 2010 +0100
@@ -347,7 +347,10 @@
   let
     val {context = ctxt, facts = chained_ths, goal} = Proof.goal st
     val i = 1
-    fun change_dir (SOME dir) = Config.put Sledgehammer_Provers.dest_dir dir
+    fun change_dir (SOME dir) =
+        Config.put Sledgehammer_Provers.dest_dir dir
+        #> Config.put SMT_Config.debug_files
+          (dir ^ "/" ^ ATP_Problem.timestamp () ^ "_" ^ serial_string ())
       | change_dir NONE = I
     val st' =
       st |> Proof.map_context