src/Pure/System/options.scala

   val string: Options.Access[String] =
     new Options.Access[String](this) {
       def apply(name: String): String = get(name, Options.String, Some(_))
       def update(name: String, x: String): Options = put(name, Options.String, x)
     }
-
-  def proper_string(name: String): Option[String] =
-    Library.proper_string(string(name))
 
   def seconds(name: String): Time = Time.seconds(real(name))
 
 
   /* external updates */

     new Options.Access_Variable[Double](this, _.real)
 
   val string: Options.Access_Variable[String] =
     new Options.Access_Variable[String](this, _.string)
 
-  def proper_string(name: String): Option[String] =
-    Library.proper_string(string(name))
-
   def seconds(name: String): Time = value.seconds(name)
 }