src/Pure/General/json.scala
changeset 71776 5ef7f374e0f8
parent 71601 97ccf48c2f0c
child 73340 0ffcad1f6130
--- a/src/Pure/General/json.scala	Tue Apr 21 19:07:49 2020 +0200
+++ b/src/Pure/General/json.scala	Tue Apr 21 22:04:15 2020 +0200
@@ -29,7 +29,7 @@
 
     def apply(entries: Entry*): Object.T = Map(entries:_*)
 
-    def unapply(obj: T): Option[Object.T] =
+    def unapply(obj: Any): Option[Object.T] =
       obj match {
         case m: Map[_, _] if m.keySet.forall(_.isInstanceOf[String]) =>
           Some(m.asInstanceOf[Object.T])