src/Pure/PIDE/xml.scala

--- a/src/Pure/PIDE/xml.scala	Mon May 08 14:08:27 2017 +0200
+++ b/src/Pure/PIDE/xml.scala	Mon May 08 14:30:37 2017 +0200
@@ -31,7 +31,7 @@
       if (more_attributes.isEmpty) this
       else Elem(markup.update_properties(more_attributes), body)
 
-    def + (att: Attribute): Tree = Elem(markup + att, body)
+    def + (att: Attribute): Elem = Elem(markup + att, body)
   }
   case class Text(content: String) extends Tree