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