tuned signature;

--- a/src/Pure/General/properties.scala	Tue May 29 16:39:42 2012 +0200
+++ b/src/Pure/General/properties.scala	Tue May 29 17:54:34 2012 +0200
@@ -52,7 +52,7 @@
       props.find(_._1 == name).map(_._2)
   }
 
-  class Int(name: java.lang.String)
+  class Int(val name: java.lang.String)
   {
     def apply(value: scala.Int): T = List((name, Value.Int(value)))
     def unapply(props: T): Option[scala.Int] =
@@ -62,7 +62,7 @@
       }
   }
 
-  class Long(name: java.lang.String)
+  class Long(val name: java.lang.String)
   {
     def apply(value: scala.Long): T = List((name, Value.Long(value)))
     def unapply(props: T): Option[scala.Long] =
@@ -72,7 +72,7 @@
       }
   }
 
-  class Double(name: java.lang.String)
+  class Double(val name: java.lang.String)
   {
     def apply(value: scala.Double): T = List((name, Value.Double(value)))
     def unapply(props: T): Option[scala.Double] =