src/Pure/library.ML
changeset 40936 10aeae27c7a6
parent 40930 500171e7aa59
child 41489 8e2b8649507d
     1.1 --- a/src/Pure/library.ML	Fri Dec 03 17:18:41 2010 +0100
     1.2 +++ b/src/Pure/library.ML	Fri Dec 03 17:29:27 2010 +0100
     1.3 @@ -727,13 +727,11 @@
     1.4  (*simple quoting (does not escape special chars)*)
     1.5  val quote = enclose "\"" "\"";
     1.6  
     1.7 -(*space_implode "..." (Symbol.explode "hello") = "h...e...l...l...o"*)
     1.8  fun space_implode a bs = implode (separate a bs);
     1.9  
    1.10  val commas = space_implode ", ";
    1.11  val commas_quote = commas o map quote;
    1.12  
    1.13 -(*concatenate messages, one per line, into a string*)
    1.14  val cat_lines = space_implode "\n";
    1.15  
    1.16  (*space_explode "." "h.e..l.lo" = ["h", "e", "", "l", "lo"]*)