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