| changeset 59469 | fb393ecde29d |
| parent 59176 | 8cf1bad1c2e7 |
| child 60924 | 610794dff23c |
--- a/src/Pure/library.ML Thu Jan 29 15:21:16 2015 +0100 +++ b/src/Pure/library.ML Thu Jan 29 15:27:29 2015 +0100 @@ -708,7 +708,7 @@ val cartouche = enclose "\\<open>" "\\<close>"; -fun space_implode a bs = implode (separate a bs); +val space_implode = String.concatWith; val commas = space_implode ", "; val commas_quote = commas o map quote;