author | krauss |
Fri, 03 Dec 2010 10:17:55 +0100 | |
changeset 40930 | 500171e7aa59 |
parent 40929 | 7ff03a5e044f |
child 40933 | 5cd8464dccbb |
child 40952 | 580b1a30994c |
--- 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 ", ";