really fixed comment (cf. 7abeb749ae99)
authorkrauss
Fri Dec 03 10:17:55 2010 +0100 (2010-12-03)
changeset 40930500171e7aa59
parent 40929 7ff03a5e044f
child 40933 5cd8464dccbb
child 40952 580b1a30994c
really fixed comment (cf. 7abeb749ae99)
src/Pure/library.ML
     1.1 --- a/src/Pure/library.ML	Fri Dec 03 10:03:13 2010 +0100
     1.2 +++ b/src/Pure/library.ML	Fri Dec 03 10:17:55 2010 +0100
     1.3 @@ -727,7 +727,7 @@
     1.4  (*simple quoting (does not escape special chars)*)
     1.5  val quote = enclose "\"" "\"";
     1.6  
     1.7 -(*space_implode "..." (space_explode "hello") = "h...e...l...l...o"*)
     1.8 +(*space_implode "..." (Symbol.explode "hello") = "h...e...l...l...o"*)
     1.9  fun space_implode a bs = implode (separate a bs);
    1.10  
    1.11  val commas = space_implode ", ";