src/Pure/General/xml.ML
changeset 14928 b8c1783c9101
parent 14910 f145696d4bb5
child 14969 3d9126cbf0e6
--- 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 = "]]>"