# HG changeset patch
# User haftmann
# Date 1284747187 -7200
# Node ID fafabbcd808c3514591575b80408cfb34823b653
# Parent  49194c9b0dd42e86a3301fbcf84d390184887e58# Parent  cf61ec140c4dc51dab228fb63b937b52c22dad7d
merged

diff -r cf61ec140c4d -r fafabbcd808c src/Tools/Code/code_printer.ML
--- a/src/Tools/Code/code_printer.ML	Fri Sep 17 17:31:20 2010 +0200
+++ b/src/Tools/Code/code_printer.ML	Fri Sep 17 20:13:07 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";