# HG changeset patch
# User wenzelm
# Date 1087073211 -7200
# Node ID b8c1783c910143f969d697b88a1c7aba6f4e0710
# Parent  66d797e1b950ac136be21f698e4e6509c258fbe5
Library.translate_string;

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 = "]]>"