# HG changeset patch
# User krauss
# Date 1291367875 -3600
# Node ID 500171e7aa59099e3588a45dc67e7f4ffd30b79d
# Parent  7ff03a5e044f0c9440dfa786e0f067f42222a090
really fixed comment (cf. 7abeb749ae99)

diff -r 7ff03a5e044f -r 500171e7aa59 src/Pure/library.ML
--- 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 ", ";