# HG changeset patch
# User bulwahn
# Date 1291362047 -3600
# Node ID 7abeb749ae99f45c04076eac606baaa68b5dd28d
# Parent  a9be7f26b4e65b72291cfd451ee1852cdd031207
fixing comment in library

diff -r a9be7f26b4e6 -r 7abeb749ae99 src/Pure/library.ML
--- 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 ", ";