--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Thu Nov 25 00:32:30 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Thu Nov 25 12:11:12 2010 +0100
@@ -482,9 +482,9 @@
| SOME (SMT_Failure.Abnormal_Termination code) =>
(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 ^ "."
- |> (if debug then error else warning)
+ " fact" ^ plural_s num_facts ^ " terminated abnormally with \
+ \exit code " ^ string_of_int code ^ "."
+ |> warning
else
();
true (* kind of *))