diff -r 6d203f6f0e8d -r 38ff9c8a7de0 src/Pure/General/xml.ML
--- a/src/Pure/General/xml.ML	Fri May 07 13:40:24 2004 +0200
+++ b/src/Pure/General/xml.ML	Fri May 07 13:42:08 2004 +0200
@@ -57,7 +57,7 @@
     Elem of string * (string * string) list * tree list
   | Text of string;
 
-fun attribute (a, x) = a ^ " = " ^ "\"" (text x) "\"";
+fun attribute (a, x) = a ^ " = \"" ^ (text x) ^ "\"";
 
 fun element name atts cs =
   let val elem = space_implode " " (name :: map attribute atts) in