src/HOL/Tools/Predicate_Compile/code_prolog.ML

   Scan.repeat (Scan.one
     (fn s => Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s orelse Symbol.is_ascii_quasi s))
 
 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
 
 val is_var_ident =
   forall (fn s => Symbol.is_ascii_upper s orelse Symbol.is_ascii_digit s orelse Symbol.is_ascii_quasi s)