# HG changeset patch
# User blanchet
# Date 1391370831 -3600
# Node ID 0ff946f0b764edbb35ae81b942009c2b733b6e4f
# Parent  235205726737eaf40572a66826e339434e9d78fd
tuning

diff -r 235205726737 -r 0ff946f0b764 src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Sun Feb 02 20:53:51 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Sun Feb 02 20:53:51 2014 +0100
@@ -174,16 +174,12 @@
     fun split_time s =
       let
         val split = String.tokens (fn c => str c = "\n")
-        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 (output, t) = s |> split |> (try split_last #> the_default ([], "0")) |>> cat_lines
+        val num = Scan.many1 Symbol.is_ascii_digit >> (fst o read_int)
         val digit = Scan.one Symbol.is_ascii_digit
-        val num3 = as_num (digit ::: digit ::: (digit >> single))
+        val num3 = digit ::: digit ::: (digit >> single) >> (fst o read_int)
         val time = num --| Scan.$$ "." -- num3 >> (fn (a, b) => a * 1000 + b)
-        val as_time =
-          raw_explode #> Scan.read Symbol.stopper time #> the_default 0
+        val as_time = raw_explode #> Scan.read Symbol.stopper time #> the_default 0
       in (output, as_time t |> Time.fromMilliseconds) end
 
     fun run () =
@@ -220,7 +216,7 @@
 
         fun run_slice time_left (cache_key, cache_value) (slice, (time_frac,
             (key as ((best_max_facts, best_fact_filter), format, best_type_enc, best_lam_trans,
-                     best_uncurried_aliases),
+               best_uncurried_aliases),
              extra))) =
           let
             val effective_fact_filter = fact_filter |> the_default best_fact_filter