standardized String.concat towards implode (cf. c37a1f29bbc0)
authorbulwahn
Sat, 09 Jul 2011 21:09:09 +0200
changeset 43735 9b88fd07b912
parent 43734 ea147bec4f72
child 43736 d2f7af6e993c
standardized String.concat towards implode (cf. c37a1f29bbc0)
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