--- a/src/Pure/System/options.scala Wed Sep 26 17:40:45 2018 +0200
+++ b/src/Pure/System/options.scala Wed Sep 26 22:07:35 2018 +0200
@@ -280,11 +280,7 @@
}
val string = new String_Access
- class Seconds_Access
- {
- def apply(name: String): Time = Time.seconds(real(name))
- }
- val seconds = new Seconds_Access
+ def seconds(name: String): Time = Time.seconds(real(name))
/* external updates */
@@ -447,9 +443,5 @@
}
val string = new String_Access
- class Seconds_Access
- {
- def apply(name: String): Time = value.seconds(name)
- }
- val seconds = new Seconds_Access
+ def seconds(name: String): Time = value.seconds(name)
}