| changeset 43735 | 9b88fd07b912 |
| parent 43324 | 2b47822868e4 |
| child 43850 | 7f2cbc713344 |
--- 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