src/Pure/General/yxml.scala
changeset 38231 968844caaff9
parent 38230 ed147003de4b
child 38234 4b610fbb2d83
--- a/src/Pure/General/yxml.scala	Sat Aug 07 22:09:52 2010 +0200
+++ b/src/Pure/General/yxml.scala	Sat Aug 07 22:43:57 2010 +0200
@@ -117,7 +117,7 @@
   /* failsafe parsing */
 
   private def markup_failsafe(source: CharSequence) =
-    XML.Elem (Markup(Markup.MALFORMED, Nil),
+    XML.elem (Markup.MALFORMED,
       List(XML.Text(source.toString.replace(X_string, "\\<^X>").replace(Y_string, "\\<^Y>"))))
 
   def parse_body_failsafe(source: CharSequence): List[XML.Tree] =