# HG changeset patch
# User blanchet
# Date 1271687392 -7200
# Node ID ed7306094efe36e9bcfb739db1a2a157a8a727ac
# Parent  fcef9196ace5f2b40ab80359bedbb2c5a7204092
cosmetics

diff -r fcef9196ace5 -r ed7306094efe src/HOL/Tools/ATP_Manager/atp_manager.ML
--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML	Mon Apr 19 15:24:57 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML	Mon Apr 19 16:29:52 2010 +0200
@@ -335,7 +335,7 @@
 fun start_prover (params as {timeout, ...}) birth_time death_time i
                  relevance_override proof_state name =
   (case get_prover (Proof.theory_of proof_state) name of
-    NONE => warning ("Unknown ATP: " ^ quote name)
+    NONE => warning ("Unknown ATP: " ^ quote name ^ ".")
   | SOME prover =>
       let
         val {context = ctxt, facts, goal} = Proof.goal proof_state;
@@ -354,7 +354,7 @@
             val message = #message (prover params timeout problem)
               handle Sledgehammer_HOL_Clause.TRIVIAL =>
                   metis_line i n []
-                | ERROR msg => ("Error: " ^ msg);
+                | ERROR msg => "Error: " ^ msg ^ ".\n";
             val _ = unregister params message (Thread.self ());
           in () end);
       in () end);