diff -r ecf80e37ed1a -r 1cb0ad6f9a2d src/Pure/General/time.scala
--- a/src/Pure/General/time.scala	Wed Aug 18 23:04:58 2021 +0200
+++ b/src/Pure/General/time.scala	Thu Aug 19 12:01:57 2021 +0200
@@ -14,8 +14,8 @@
 object Time
 {
   def seconds(s: Double): Time = new Time((s * 1000.0).round)
-  def minutes(s: Double): Time = new Time((s * 60000.0).round)
-  def ms(m: Long): Time = new Time(m)
+  def minutes(m: Double): Time = new Time((m * 60000.0).round)
+  def ms(ms: Long): Time = new Time(ms)
   def hms(h: Int, m: Int, s: Double): Time = seconds(s + 60 * m + 3600 * h)
 
   def now(): Time = ms(System.currentTimeMillis())