diff -r 66d797e1b950 -r b8c1783c9101 src/Pure/General/xml.ML
--- a/src/Pure/General/xml.ML	Sat Jun 12 22:46:39 2004 +0200
+++ b/src/Pure/General/xml.ML	Sat Jun 12 22:46:51 2004 +0200
@@ -41,7 +41,7 @@
   | decode """ = "\""
   | decode c = c;
 
-val text = String.translate (encode o String.str);
+val text = Library.translate_string encode;
 
 val cdata_open  = "<![CDATA["
 val cdata_close = "]]>"