src/Pure/library.scala

--- a/src/Pure/library.scala	Fri Jul 20 11:52:20 2012 +0200
+++ b/src/Pure/library.scala	Fri Jul 20 12:00:08 2012 +0200
@@ -100,7 +100,7 @@
 
   def quote(s: String): String = "\"" + s + "\""
   def commas(ss: Iterable[String]): String = ss.iterator.mkString(", ")
-  def commas_quote(ss: Iterable[String]): String = ss.iterator.mkString("\"", ", ", "\"")
+  def commas_quote(ss: Iterable[String]): String = ss.iterator.map(quote).mkString(", ")
 
 
   /* reverse CharSequence */