1.1 --- a/src/Pure/General/xml.ML	Fri May 07 13:40:24 2004 +0200
     1.2 +++ b/src/Pure/General/xml.ML	Fri May 07 13:42:08 2004 +0200
     1.3 @@ -57,7 +57,7 @@
     1.4      Elem of string * (string * string) list * tree list
     1.5    | Text of string;
     1.6  
     1.7 -fun attribute (a, x) = a ^ " = " ^ "\"" (text x) "\"";
     1.8 +fun attribute (a, x) = a ^ " = \"" ^ (text x) ^ "\"";
     1.9  
    1.10  fun element name atts cs =
    1.11    let val elem = space_implode " " (name :: map attribute atts) in