author | bulwahn |
Fri, 03 Dec 2010 08:40:47 +0100 | |
changeset 40925 | 7abeb749ae99 |
parent 40924 | a9be7f26b4e6 |
child 40926 | c600f6ae4b09 |
--- 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 ", ";