tuned message (cf. ML version);
authorwenzelm
Wed Mar 07 23:21:24 2012 +0100 (2012-03-07 ago)
changeset 46832050e344825c8
parent 46831 4a6085849a37
child 46835 be56a254d880
tuned message (cf. ML version);
src/Pure/PIDE/yxml.ML
     1.1 --- a/src/Pure/PIDE/yxml.ML	Wed Mar 07 20:49:18 2012 +0100
     1.2 +++ b/src/Pure/PIDE/yxml.ML	Wed Mar 07 23:21:24 2012 +0100
     1.3 @@ -92,7 +92,7 @@
     1.4  
     1.5  (* structural errors *)
     1.6  
     1.7 -fun err msg = raise Fail ("Malformed YXML encoding: " ^ msg);
     1.8 +fun err msg = raise Fail ("Malformed YXML: " ^ msg);
     1.9  fun err_attribute () = err "bad attribute";
    1.10  fun err_element () = err "bad element";
    1.11  fun err_unbalanced "" = err "unbalanced element"