# HG changeset patch
# User blanchet
# Date 1271493729 -7200
# Node ID 500fc43d5537585d49ca37512d60302aa50cb74a
# Parent  ba06ef722163fda04dd71b2d4ddc112dfe0ead7b
added missing \n in output

diff -r ba06ef722163 -r 500fc43d5537 src/HOL/Tools/ATP_Manager/atp_wrapper.ML
--- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Fri Apr 16 21:18:05 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Sat Apr 17 10:42:09 2010 +0200
@@ -140,7 +140,7 @@
         ()
       else
         File.write (Path.explode (Path.implode probfile ^ "_proof"))
-                   ("#" ^ timestamp () ^ "\n" ^ proof)
+                   ("% " ^ timestamp () ^ "\n" ^ proof)
 
     val (((proof, atp_run_time_in_msecs), rc), conj_pos) =
       with_path cleanup export run_on (prob_pathname subgoal);
@@ -149,8 +149,8 @@
     val failure = find_failure failure_strs proof;
     val success = rc = 0 andalso is_none failure;
     val (message, relevant_thm_names) =
-      if is_some failure then ("ATP failed to find a proof.", [])
-      else if rc <> 0 then ("ATP error: " ^ proof ^ ".", [])
+      if is_some failure then ("ATP failed to find a proof.\n", [])
+      else if rc <> 0 then ("ATP error: " ^ proof ^ ".\n", [])
       else
         (produce_answer name (proof, internal_thm_names, conj_pos, ctxt, th,
                               subgoal));