src/Pure/ML/ml_syntax.scala

--- a/src/Pure/ML/ml_syntax.scala	Fri Apr 07 18:26:30 2017 +0200
+++ b/src/Pure/ML/ml_syntax.scala	Fri Apr 07 19:35:39 2017 +0200
@@ -46,6 +46,12 @@
     quote(UTF8.bytes(str).iterator.map(print_chr(_)).mkString)
 
 
+  /* pair */
+
+  def print_pair[A, B](f: A => String, g: B => String)(pair: (A, B)): String =
+    "(" + f(pair._1) + ", " + g(pair._2) + ")"
+
+
   /* list */
 
   def print_list[A](f: A => String)(list: List[A]): String =