# HG changeset patch
# User boehmes
# Date 1289856248 -3600
# Node ID bbcb7aa90afc7530392be2d69afb7dc883571f67
# Parent  0125cbb5d3c7828a9e23e1a1499ca8407cc5a0f4# Parent  9597b93a8c00ae77dd1936434b755d1b0e5eb420
merged

diff -r 0125cbb5d3c7 -r bbcb7aa90afc src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Mon Nov 15 22:23:28 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Mon Nov 15 22:24:08 2010 +0100
@@ -516,6 +516,7 @@
         "The SMT solver terminated abnormally with exit code " ^
         string_of_int code ^ "."
       | SOME (SMT_Failure.Counterexample _) => "The SMT problem is unprovable."
+      | SOME SMT_Failure.Out_Of_Memory => "The SMT solver ran out of memory."
       | SOME failure =>
         SMT_Failure.string_of_failure ctxt failure
     val outcome = outcome |> Option.map failure_from_smt_failure (* FIXME *)