src/HOL/Tools/Sledgehammer/sledgehammer_shrink.ML

 (*  Title:      HOL/Tools/Sledgehammer/sledgehammer_shrink.ML
     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 =
 sig
   type isar_step = Sledgehammer_Proof.isar_step

 end
 
 structure Sledgehammer_Shrink (* : SLEDGEHAMMER_SHRINK *) =
 struct
 
+open Sledgehammer_Util
 open Sledgehammer_Proof
 
 (* Parameters *)
 val merge_timeout_slack = 1.2
 

         (case get j metis_time |> Lazy.force of
           NONE => (NONE, metis_time)
         | 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)
             | some_t12 =>
               (SOME s12, metis_time