1.1 --- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Fri Apr 16 21:18:05 2010 +0200
     1.2 +++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Sat Apr 17 10:42:09 2010 +0200
     1.3 @@ -140,7 +140,7 @@
     1.4          ()
     1.5        else
     1.6          File.write (Path.explode (Path.implode probfile ^ "_proof"))
     1.7 -                   ("#" ^ timestamp () ^ "\n" ^ proof)
     1.8 +                   ("% " ^ timestamp () ^ "\n" ^ proof)
     1.9  
    1.10      val (((proof, atp_run_time_in_msecs), rc), conj_pos) =
    1.11        with_path cleanup export run_on (prob_pathname subgoal);
    1.12 @@ -149,8 +149,8 @@
    1.13      val failure = find_failure failure_strs proof;
    1.14      val success = rc = 0 andalso is_none failure;
    1.15      val (message, relevant_thm_names) =
    1.16 -      if is_some failure then ("ATP failed to find a proof.", [])
    1.17 -      else if rc <> 0 then ("ATP error: " ^ proof ^ ".", [])
    1.18 +      if is_some failure then ("ATP failed to find a proof.\n", [])
    1.19 +      else if rc <> 0 then ("ATP error: " ^ proof ^ ".\n", [])
    1.20        else
    1.21          (produce_answer name (proof, internal_thm_names, conj_pos, ctxt, th,
    1.22                                subgoal));