diff -r e8990d0e3965 -r 73939a9b70a3 src/Pure/General/multi_map.scala
--- a/src/Pure/General/multi_map.scala	Tue Aug 02 11:49:30 2016 +0200
+++ b/src/Pure/General/multi_map.scala	Tue Aug 02 17:35:18 2016 +0200
@@ -8,6 +8,7 @@
 package isabelle
 
 
+import scala.collection.GenTraversableOnce
 import scala.collection.generic.{ImmutableMapFactory, CanBuildFrom}
 
 
@@ -75,6 +76,9 @@
 
   def + [B1 >: B](p: (A, B1)): Multi_Map[A, B1] = insert(p._1, p._2)
 
+  override def ++ [B1 >: B](entries: GenTraversableOnce[(A, B1)]): Multi_Map[A, B1] =
+    (this.asInstanceOf[Multi_Map[A, B1]] /: entries)(_ + _)
+
   def - (a: A): Multi_Map[A, B] =
     if (rep.isDefinedAt(a)) new Multi_Map(rep - a) else this
 }