# HG changeset patch
# User blanchet
# Date 1335293709 -7200
# Node ID 63c939dcd0555497aaad632c81c82139246509ec
# Parent  d349c8ff3ace37e30179868d32f498d67c58bea6
made "split_last" more robust in the face of obscure low-level errors

diff -r d349c8ff3ace -r 63c939dcd055 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Apr 24 20:55:09 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Apr 24 20:55:09 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