src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML

             |> Random_Engine.run))*)
         Pos_Random_DSeq =>
           let
             val [nrandom, size, depth] = arguments
           in
-            rpair NONE (TimeLimit.timeLimit (Time.fromSeconds 20) (fn () => fst (DSequence.yieldn k
+            rpair NONE (TimeLimit.timeLimit (seconds 20.0) (fn () => fst (DSequence.yieldn k
               (Code_Runtime.dynamic_value_strict (Dseq_Random_Result.get, put_dseq_random_result, "Predicate_Compile_Core.put_dseq_random_result")
                 thy NONE (fn proc => fn g => fn nrandom => fn size => fn s => g nrandom size s |>> DSequence.map proc)
                   t' [] nrandom size
                 |> Random_Engine.run)
               depth true)) ())
           end
       | DSeq =>
-          rpair NONE (TimeLimit.timeLimit (Time.fromSeconds 20) (fn () => fst (DSequence.yieldn k
+          rpair NONE (TimeLimit.timeLimit (seconds 20.0) (fn () => fst (DSequence.yieldn k
             (Code_Runtime.dynamic_value_strict (Dseq_Result.get, put_dseq_result, "Predicate_Compile_Core.put_dseq_result")
               thy NONE DSequence.map t' []) (the_single arguments) true)) ())
       | Pos_Generator_DSeq =>
           let
             val depth = (the_single arguments)
           in
-            rpair NONE (TimeLimit.timeLimit (Time.fromSeconds 20) (fn () => fst (Lazy_Sequence.yieldn k
+            rpair NONE (TimeLimit.timeLimit (seconds 20.0) (fn () => fst (Lazy_Sequence.yieldn k
               (Code_Runtime.dynamic_value_strict (New_Dseq_Result.get, put_new_dseq_result, "Predicate_Compile_Core.put_new_dseq_result")
               thy NONE (fn proc => fn g => fn depth => g depth |> Lazy_Sequence.mapa proc)
               t' [] depth))) ())
           end
       | New_Pos_Random_DSeq =>
           let
             val [nrandom, size, depth] = arguments
             val seed = Random_Engine.next_seed ()
           in
             if stats then
-              apsnd (SOME o accumulate) (split_list (TimeLimit.timeLimit (Time.fromSeconds 20)
+              apsnd (SOME o accumulate) (split_list (TimeLimit.timeLimit (seconds 20.0)
               (fn () => fst (Lazy_Sequence.yieldn k
                 (Code_Runtime.dynamic_value_strict
                   (Lseq_Random_Stats_Result.get, put_lseq_random_stats_result, "Predicate_Compile_Core.put_lseq_random_stats_result")
                   thy NONE
                   (fn proc => fn g => fn nrandom => fn size => fn s => fn depth => g nrandom size s depth
                     |> Lazy_Sequence.mapa (apfst proc))
                     t' [] nrandom size seed depth))) ()))
             else rpair NONE
-              (TimeLimit.timeLimit (Time.fromSeconds 20) (fn () => fst (Lazy_Sequence.yieldn k
+              (TimeLimit.timeLimit (seconds 20.0) (fn () => fst (Lazy_Sequence.yieldn k
                 (Code_Runtime.dynamic_value_strict
                   (Lseq_Random_Result.get, put_lseq_random_result, "Predicate_Compile_Core.put_lseq_random_result")
                   thy NONE 
                   (fn proc => fn g => fn nrandom => fn size => fn s => fn depth => g nrandom size s depth
                     |> Lazy_Sequence.mapa proc)
                     t' [] nrandom size seed depth))) ())
           end
       | _ =>
-          rpair NONE (TimeLimit.timeLimit (Time.fromSeconds 20) (fn () => fst (Predicate.yieldn k
+          rpair NONE (TimeLimit.timeLimit (seconds 20.0) (fn () => fst (Predicate.yieldn k
             (Code_Runtime.dynamic_value_strict (Pred_Result.get, put_pred_result, "Predicate_Compile_Core.put_pred_result")
               thy NONE Predicate.map t' []))) ()))
      handle TimeLimit.TimeOut => error "Reached timeout during execution of values"
   in ((T, ts), statistics) end;