# HG changeset patch
# User bulwahn
# Date 1310238549 -7200
# Node ID 9b88fd07b912ecb4b1c868596a6e004ee7c3b9c3
# Parent  ea147bec4f72db73bde54d88ffa7b40f54040807
standardized String.concat towards implode (cf. c37a1f29bbc0)

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