tuned signature;

--- a/src/Pure/General/json.scala	Fri Oct 27 15:49:09 2017 +0200
+++ b/src/Pure/General/json.scala	Fri Oct 27 16:21:29 2017 +0200
@@ -257,10 +257,12 @@
 
   /* object values */
 
+  val empty: Map[String, T] = Map.empty
+
   def optional(entry: (String, Option[T])): Map[String, T] =
     entry match {
       case (name, Some(x)) => Map(name -> x)
-      case (_, None) => Map.empty
+      case (_, None) => empty
     }
 
   def value(obj: T, name: String): Option[T] =