# HG changeset patch
# User wenzelm
# Date 1537992455 -7200
# Node ID d05defa39e3d5b918d18d559c3e095745a367014
# Parent  337b8ce5ff8da09b0368506206440db3ee7fd205
tuned signature;

diff -r 337b8ce5ff8d -r d05defa39e3d src/Pure/System/options.scala
--- 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)
 }