src/Pure/General/time.scala

--- a/src/Pure/General/time.scala	Sat Aug 13 12:05:53 2016 +0200
+++ b/src/Pure/General/time.scala	Sat Aug 13 12:06:11 2016 +0200
@@ -15,6 +15,8 @@
 {
   def seconds(s: Double): Time = new Time((s * 1000.0).round)
   def ms(m: Long): Time = new Time(m)
+  def hours_minutes_seconds(h: Int, m: Int, s: Double): Time = seconds(s + 60 * m + 3600 * h)
+
   def now(): Time = ms(System.currentTimeMillis())
 
   val zero: Time = ms(0)