# HG changeset patch
# User immler@in.tum.de
# Date 1245683228 -7200
# Node ID fda2cf4fef5871e05a9f7716433d405346e7ceec
# Parent  f28b7365fabfdd348e7ed23da18fe0861aad4c87
export proof when exporting problemfile

diff -r f28b7365fabf -r fda2cf4fef58 src/HOL/Tools/atp_wrapper.ML
--- a/src/HOL/Tools/atp_wrapper.ML	Mon Jun 22 17:07:08 2009 +0200
+++ b/src/HOL/Tools/atp_wrapper.ML	Mon Jun 22 17:07:08 2009 +0200
@@ -85,8 +85,13 @@
       else error ("Bad executable: " ^ Path.implode cmd)
     val (proof, rc) = system_out (cmdline ^ " " ^ fname)
 
-    (* remove *temporary* files *)
-    val _ = if destdir' = "" then OS.FileSys.remove fname else ()
+    (* if problemfile has not been exported, delete problemfile; otherwise export proof, too *)
+    val _ =
+      if destdir' = "" then OS.FileSys.remove fname
+      else
+        let val out = TextIO.openOut (fname ^ "_proof")
+        val _ = TextIO.output (out, proof)
+        in TextIO.closeOut out end
     
     (* check for success and print out some information on failure *)
     val failure = find_failure proof