diff -r 57f379ef662f -r efa178abe023 src/Pure/ML/ml_syntax.scala
--- a/src/Pure/ML/ml_syntax.scala	Mon Mar 07 14:53:28 2016 +0100
+++ b/src/Pure/ML/ml_syntax.scala	Mon Mar 07 15:21:50 2016 +0100
@@ -33,4 +33,7 @@
 
   def print_string_raw(str: String): String =
     quote(UTF8.bytes(str).iterator.map(print_chr(_)).mkString)
+
+  def print_list[A](f: A => String)(list: List[A]): String =
+    "[" + commas(list.map(f)) + "]"
 }