merged

--- a/src/HOL/Tools/ATP/atp_systems.ML	Tue Apr 24 19:14:03 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Tue Apr 24 23:03:59 2012 +0200
@@ -303,8 +303,7 @@
    known_failures =
      known_szs_status_failures @
      [(TimedOut, "Failure: Resource limit exceeded (time)"),
-      (TimedOut, "time limit exceeded"),
-      (OutOfResources, "# Cannot determine problem status")],
+      (TimedOut, "time limit exceeded")],
    conj_sym_kind = Hypothesis,
    prem_kind = Conjecture,
    best_slices = fn ctxt =>

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Apr 24 19:14:03 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Apr 24 23:03:59 2012 +0200
@@ -611,7 +611,9 @@
     fun split_time s =
       let
         val split = String.tokens (fn c => str c = "\n")
-        val (output, t) = s |> split |> split_last |> apfst cat_lines
+        val (output, t) =
+          s |> split |> (try split_last #> the_default ([], "0"))
+            |>> cat_lines
         fun as_num f = f >> (fst o read_int)
         val num = as_num (Scan.many1 Symbol.is_ascii_digit)
         val digit = Scan.one Symbol.is_ascii_digit
@@ -619,10 +621,7 @@
         val time = num --| Scan.$$ "." -- num3 >> (fn (a, b) => a * 1000 + b)
         val as_time =
           raw_explode #> Scan.read Symbol.stopper time #> the_default 0
-      in
-        (output,
-         as_time t |> Time.fromMilliseconds)
-      end
+      in (output, as_time t |> Time.fromMilliseconds) end
     fun run_on prob_file =
       case find_first (forall (fn var => getenv var = ""))
                       (fst exec :: required_vars) of