# HG changeset patch
# User blanchet
# Date 1290683472 -3600
# Node ID 7fa054c3f810b4c0d443ca79e0312260a06800a1
# Parent  a68f64f998328724cd183cd7e917b024b7329aba
make "debug" mode of Sledgehammer/SMT more liberal

diff -r a68f64f99832 -r 7fa054c3f810 src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- 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 *))