src/Pure/General/multi_map.scala

--- a/src/Pure/General/multi_map.scala	Fri Feb 14 11:10:28 2014 +0100
+++ b/src/Pure/General/multi_map.scala	Fri Feb 14 14:39:44 2014 +0100
@@ -25,6 +25,8 @@
 {
   /* Multi_Map operations */
 
+  def iterator_list: Iterator[(A, List[B])] = rep.iterator
+
   def get_list(a: A): List[B] = rep.getOrElse(a, Nil)
 
   def insert[B1 >: B](a: A, b: B1): Multi_Map[A, B1] =