removed confusing comments (cf. 500171e7aa59);
authorwenzelm
Fri, 03 Dec 2010 17:29:27 +0100
changeset 40936 10aeae27c7a6
parent 40935 f48c5b951042
child 40937 e2e0ef28d3f8
removed confusing comments (cf. 500171e7aa59);
src/Pure/library.ML
--- a/src/Pure/library.ML	Fri Dec 03 17:18:41 2010 +0100
+++ b/src/Pure/library.ML	Fri Dec 03 17:29:27 2010 +0100
@@ -727,13 +727,11 @@
 (*simple quoting (does not escape special chars)*)
 val quote = enclose "\"" "\"";
 
-(*space_implode "..." (Symbol.explode "hello") = "h...e...l...l...o"*)
 fun space_implode a bs = implode (separate a bs);
 
 val commas = space_implode ", ";
 val commas_quote = commas o map quote;
 
-(*concatenate messages, one per line, into a string*)
 val cat_lines = space_implode "\n";
 
 (*space_explode "." "h.e..l.lo" = ["h", "e", "", "l", "lo"]*)