src/Pure/PIDE/xml.ML
changeset 48769 e3b7087bb923
parent 47199 15ede9f1da3f
child 49599 e716209814b3
--- a/src/Pure/PIDE/xml.ML	Sat Aug 11 17:24:21 2012 +0200
+++ b/src/Pure/PIDE/xml.ML	Sat Aug 11 17:40:33 2012 +0200
@@ -224,7 +224,7 @@
   (case Scan.finite Symbol.stopper (Scan.error (!! (err (fn () => "Malformed element"))
       (blanks |-- parse_document --| blanks))) (raw_explode s) of
     (x, []) => x
-  | (_, ys) => error ("XML parsing error: Unprocessed input\n" ^ Symbol.beginning 100 ys));
+  | (_, ys) => error ("XML parsing error: unprocessed input\n" ^ Symbol.beginning 100 ys));
 
 end;