diff -r ea147bec4f72 -r 9b88fd07b912 src/HOL/Tools/Predicate_Compile/code_prolog.ML
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Sat Jul 09 19:29:25 2011 +0200
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Sat Jul 09 21:09:09 2011 +0200
@@ -814,7 +814,7 @@
 
 fun dest_Char (Symbol.Char s) = s
 
-val string_of = concat o map (dest_Char o Symbol.decode)
+val string_of = implode o map (dest_Char o Symbol.decode)
 
 val is_atom_ident = forall Symbol.is_ascii_lower