changeset 32952 | aeb1e44fbc19 |
parent 26537 | 188961eb1f08 |
child 32960 | 69916a850301 |
--- a/src/HOL/Import/xml.ML Thu Oct 15 23:10:35 2009 +0200 +++ b/src/HOL/Import/xml.ML Thu Oct 15 23:28:10 2009 +0200 @@ -137,7 +137,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 = ($$ "<" |-- scan_id --