src/Pure/General/xml.ML

--- a/src/Pure/General/xml.ML	Thu Apr 27 12:11:56 2006 +0200
+++ b/src/Pure/General/xml.ML	Thu Apr 27 15:06:35 2006 +0200
@@ -134,7 +134,7 @@
         || parse_pi >> K []
         || parse_comment >> K []) --
        Scan.optional ((* scan_whspc |-- *) parse_chars >> (single o Text)) []
-         >> op @) >> List.concat) >> op @)(* --| scan_whspc*)) xs
+         >> op @) >> flat) >> op @)(* --| scan_whspc*)) xs
 
 and parse_elem xs =
   ($$ "<" |-- Symbol.scan_id --