src/HOL/Tools/Sledgehammer/sledgehammer.ML
changeset 40556 d66403b60b3b
parent 40555 de581d7da0b6
child 40558 e75614d0a859
--- 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
                ();