| changeset 46832 | 050e344825c8 |
| parent 46831 | 4a6085849a37 |
| child 49656 | 7ff712de5747 |
--- 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"