# HG changeset patch
# User blanchet
# Date 1271443850 -7200
# Node ID 4deef08608ee0fa0d0eb3ca0d3540b0609a0d482
# Parent  bd246b00ef5a76514e03ab01df304c1252c0216d
added timestamp to proof

diff -r bd246b00ef5a -r 4deef08608ee src/HOL/Tools/ATP_Manager/atp_wrapper.ML
--- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Fri Apr 16 16:54:05 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Fri Apr 16 20:50:50 2010 +0200
@@ -20,6 +20,7 @@
 structure ATP_Wrapper : ATP_WRAPPER =
 struct
 
+open Sledgehammer_Util
 open Sledgehammer_Fact_Preprocessor
 open Sledgehammer_HOL_Clause
 open Sledgehammer_Fact_Filter
@@ -135,8 +136,11 @@
        the proof file too. *)
     fun cleanup probfile = if destdir' = "" then try File.rm probfile else NONE;
     fun export probfile (((proof, _), _), _) =
-      if destdir' = "" then ()
-      else File.write (Path.explode (Path.implode probfile ^ "_proof")) proof;
+      if destdir' = "" then
+        ()
+      else
+        File.write (Path.explode (Path.implode probfile ^ "_proof"))
+                   ("#" ^ timestamp () ^ "\n" ^ proof)
 
     val (((proof, atp_run_time_in_msecs), rc), conj_pos) =
       with_path cleanup export run_on (prob_pathname subgoal);