# HG changeset patch
# User blanchet
# Date 1289843910 -3600
# Node ID d66403b60b3bca9b2153d55cb6ee43c300db4744
# Parent  de581d7da0b63c54e5421eacf23721792c2d2447
cosmetics

diff -r de581d7da0b6 -r d66403b60b3b src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Mon Nov 15 18:56:31 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Mon Nov 15 18:58:30 2010 +0100
@@ -473,7 +473,7 @@
             (if verbose then
                "The SMT solver invoked with " ^ string_of_int num_facts ^
                " fact" ^ plural_s num_facts ^ " terminated abnormally with \
-               \exit code " ^ string_of_int code
+               \exit code " ^ string_of_int code ^ "."
                |> (if debug then error else warning)
              else
                ();