diff -r d4c8b2cf685f -r 3e9fe7a84b5d src/Pure/General/json.scala
--- a/src/Pure/General/json.scala	Tue Mar 13 19:35:08 2018 +0100
+++ b/src/Pure/General/json.scala	Tue Mar 13 20:02:09 2018 +0100
@@ -20,7 +20,9 @@
   object Object
   {
     type T = Map[String, JSON.T]
-    val empty: T = Map.empty
+    val empty: Object.T = Map.empty
+
+    def apply(entries: (String, JSON.T)*): Object.T = Map(entries:_*)
 
     def unapply(obj: T): Option[Object.T] =
       obj match {
@@ -299,7 +301,7 @@
 
   def optional(entry: (String, Option[T])): Object.T =
     entry match {
-      case (name, Some(x)) => Map(name -> x)
+      case (name, Some(x)) => Object(name -> x)
       case (_, None) => Object.empty
     }