| changeset 40925 | 7abeb749ae99 |
| parent 40733 | a71f786d20da |
| child 40930 | 500171e7aa59 |
--- a/src/Pure/library.ML Fri Dec 03 08:40:47 2010 +0100 +++ b/src/Pure/library.ML Fri Dec 03 08:40:47 2010 +0100 @@ -727,7 +727,7 @@ (*simple quoting (does not escape special chars)*) val quote = enclose "\"" "\""; -(*space_implode "..." (explode "hello") = "h...e...l...l...o"*) +(*space_implode "..." (space_explode "hello") = "h...e...l...l...o"*) fun space_implode a bs = implode (separate a bs); val commas = space_implode ", ";