--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Mon Nov 15 21:08:48 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Mon Nov 15 22:08:01 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 *)