diff -r 688a7dd22cbb -r 368399c5d87f 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