diff -r 2df717e26035 -r c36e116b578b src/Pure/General/xml.ML
--- a/src/Pure/General/xml.ML	Fri Apr 16 18:42:02 2004 +0200
+++ b/src/Pure/General/xml.ML	Fri Apr 16 18:43:36 2004 +0200
@@ -41,7 +41,7 @@
   | decode """ = "\""
   | decode c = c;
 
-val text = implode o map encode o explode;
+val text = String.translate (encode o String.str);
 
 
 (* elements *)
@@ -50,7 +50,7 @@
     Elem of string * (string * string) list * tree list
   | Text of string;
 
-fun attribute (a, x) = a ^ " = " ^ quote (text x);
+fun attribute (a, x) = a ^ " = " ^ Library.quote (text x);
 
 fun element name atts cs =
   let val elem = space_implode " " (name :: map attribute atts) in