src/Pure/pattern.ML
changeset 80910 406a85a25189
parent 70443 a21a96eda033
--- a/src/Pure/pattern.ML	Fri Sep 20 13:30:55 2024 +0200
+++ b/src/Pure/pattern.ML	Fri Sep 20 14:28:13 2024 +0200
@@ -36,7 +36,7 @@
   Syntax.string_of_term ctxt (Envir.norm_term env (subst_bounds (map Free binders, t)));
 
 fun bname binders i = fst (nth binders i);
-fun bnames binders is = space_implode " " (map (bname binders) is);
+fun bnames binders is = implode_space (map (bname binders) is);
 
 fun typ_clash context (tye,T,U) =
   if Config.get_generic context unify_trace_failure then