# HG changeset patch
# User wenzelm
# Date 1344699633 -7200
# Node ID e3b7087bb923d66914864c497a31b9a2775bda37
# Parent  abc45de5bb22838b7d7b4a5b0b7e3d1765cae2ac
tuned message;

diff -r abc45de5bb22 -r e3b7087bb923 src/Pure/PIDE/xml.ML
--- 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;