src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML

     fun knn () =
       k_nearest_neighbors dffreq num_facts num_feats depss featss max_suggs fact_idxs int_goal_feats
       |> map fst
   in
     (trace_msg ctxt (fn () => "MaSh query internal " ^ commas (map fst goal_feats) ^ " from {" ^
-       elide_string 1000 (space_implode " " (Vector.foldr (op ::) [] fact_names)) ^ "}");
+       elide_string 1000 (implode_space (Vector.foldr (op ::) [] fact_names)) ^ "}");
      (case algorithm of
        MaSh_NB => nb ()
      | MaSh_kNN => knn ()
      | MaSh_NB_kNN =>
        mesh_facts I (op =) max_suggs

     | NONE => "" (* error *))
   | unmeta_chars _ (#"%" :: _) = "" (* error *)
   | unmeta_chars accum (c :: cs) = unmeta_chars (c :: accum) cs
 
 val encode_str = String.translate meta_char
-val encode_strs = map encode_str #> space_implode " "
+val encode_strs = map encode_str #> implode_space
 
 fun decode_str s =
   if String.isSubstring "%" s then unmeta_chars [] (String.explode s) else s;
 
 fun decode_strs s =