diff -r 742435a3a992 -r 49194c9b0dd4 src/Tools/Code/code_printer.ML
--- a/src/Tools/Code/code_printer.ML	Fri Sep 17 12:26:57 2010 +0200
+++ b/src/Tools/Code/code_printer.ML	Fri Sep 17 17:17:56 2010 +0200
@@ -147,13 +147,13 @@
         else s1 ^ s ^ s2
       end;
 
-fun plain_text (XML.Elem (_, xs)) = implode (map plain_text xs)
+fun plain_text (XML.Elem (_, xs)) = maps_string "" plain_text xs
   | plain_text (XML.Text s) = s
 
 fun format presentation_names width =
   Print_Mode.setmp [code_presentationN] (Pretty.string_of_margin width)
   #> YXML.parse_body
-  #> (if null presentation_names then implode o map plain_text
+  #> (if null presentation_names then maps_string "" plain_text
       else maps_string "\n\n" (filter_presentation presentation_names false))
   #> suffix "\n";