standardized String.concat towards implode (cf. c37a1f29bbc0)
authorbulwahn
Sat Jul 09 21:09:09 2011 +0200 (2011-07-09)
changeset 437359b88fd07b912
parent 43734 ea147bec4f72
child 43736 d2f7af6e993c
standardized String.concat towards implode (cf. c37a1f29bbc0)
src/HOL/Tools/Predicate_Compile/code_prolog.ML
     1.1 --- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Sat Jul 09 19:29:25 2011 +0200
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML	Sat Jul 09 21:09:09 2011 +0200
     1.3 @@ -814,7 +814,7 @@
     1.4  
     1.5  fun dest_Char (Symbol.Char s) = s
     1.6  
     1.7 -val string_of = concat o map (dest_Char o Symbol.decode)
     1.8 +val string_of = implode o map (dest_Char o Symbol.decode)
     1.9  
    1.10  val is_atom_ident = forall Symbol.is_ascii_lower
    1.11