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