author | blanchet |
Mon, 15 Nov 2010 18:58:30 +0100 | |
changeset 40556 | d66403b60b3b |
parent 40555 | de581d7da0b6 |
child 40557 | 5534b18bce5d |
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 ();