# HG changeset patch
# User smolkas
# Date 1354101943 -3600
# Node ID 9eafa567e061728d799191bc83d3ce5bf8efbc87
# Parent  a9ec48b98734270d0e2a1c17b30dadcf1ff884fe
made use of sledgehammer_util

diff -r a9ec48b98734 -r 9eafa567e061 src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML	Wed Nov 28 12:25:43 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML	Wed Nov 28 12:25:43 2012 +0100
@@ -2,7 +2,7 @@
     Author:     Jasmin Blanchette, TU Muenchen
     Author:     Steffen Juilf Smolka, TU Muenchen
 
-Shrinking of isar proofs reconstructed from ATP proofs.
+Shrinking and preplaying of reconstructed isar proofs.
 *)
 
 signature SLEDGEHAMMER_SHRINK =
@@ -16,6 +16,7 @@
 structure Sledgehammer_Shrink (* : SLEDGEHAMMER_SHRINK *) =
 struct
 
+open Sledgehammer_Util
 open Sledgehammer_Proof
 
 (* Parameters *)
@@ -140,9 +141,7 @@
         | SOME t2 =>
           let
             val s12 = merge s1 s2
-            val timeout =
-              Time.+ (t1, t2) |> Time.toReal |> curry Real.* merge_timeout_slack
-                      |> Time.fromReal
+            val timeout = time_mult merge_timeout_slack (t1 + t2)
           in
             case try_metis timeout s12 () of
               NONE => (NONE, metis_time)