# HG changeset patch
# User wenzelm
# Date 1331158884 -3600
# Node ID 050e344825c83a5b800057356479dedbc2465c5d
# Parent  4a6085849a37fa7d57f5a447ecd43ef422808146
tuned message (cf. ML version);

diff -r 4a6085849a37 -r 050e344825c8 src/Pure/PIDE/yxml.ML
--- a/src/Pure/PIDE/yxml.ML	Wed Mar 07 20:49:18 2012 +0100
+++ b/src/Pure/PIDE/yxml.ML	Wed Mar 07 23:21:24 2012 +0100
@@ -92,7 +92,7 @@
 
 (* structural errors *)
 
-fun err msg = raise Fail ("Malformed YXML encoding: " ^ msg);
+fun err msg = raise Fail ("Malformed YXML: " ^ msg);
 fun err_attribute () = err "bad attribute";
 fun err_element () = err "bad element";
 fun err_unbalanced "" = err "unbalanced element"