# HG changeset patch
# User blanchet
# Date 1271860683 -7200
# Node ID 9a7c5b86a1052d95d04d532e35c1b91e32c6d4e8
# Parent  dbbf4d5d584d217561aec0e99cb3dbf918fe52b0
generate command-line in addition to timestamp in ATP output file, for debugging purposes

diff -r dbbf4d5d584d -r 9a7c5b86a105 src/HOL/Tools/ATP_Manager/atp_wrapper.ML
--- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Wed Apr 21 16:21:19 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Wed Apr 21 16:38:03 2010 +0200
@@ -145,7 +145,10 @@
         ()
       else
         File.write (Path.explode (Path.implode probfile ^ "_proof"))
-                   ("% " ^ timestamp () ^ "\n" ^ proof)
+                   ((if overlord then
+                       "% " ^ cmd_line probfile ^ "\n% " ^ timestamp () ^ "\n"
+                     else
+                        "") ^ proof)
 
     val (((proof, atp_run_time_in_msecs), rc), _) =
       with_path cleanup export run_on (prob_pathname subgoal);