--- a/src/Pure/General/multi_map.scala Wed Mar 03 22:48:46 2021 +0100
+++ b/src/Pure/General/multi_map.scala Thu Mar 04 15:41:46 2021 +0100
@@ -17,7 +17,7 @@
def empty[A, B]: Multi_Map[A, B] = empty_val.asInstanceOf[Multi_Map[A, B]]
def from[A, B](entries: IterableOnce[(A, B)]): Multi_Map[A, B] =
- (empty[A, B] /: entries)({ case (m, (a, b)) => m.insert(a, b) })
+ entries.foldLeft(empty[A, B]) { case (m, (a, b)) => m.insert(a, b) }
override def newBuilder[A, B]: mutable.Builder[(A, B), Multi_Map[A, B]] = new Builder[A, B]
private class Builder[A, B] extends mutable.Builder[(A, B), Multi_Map[A, B]]
@@ -63,7 +63,7 @@
if (this eq other) this
else if (isEmpty) other
else
- (this.asInstanceOf[Multi_Map[A, B1]] /: other.rep.iterator) {
+ other.rep.iterator.foldLeft(this.asInstanceOf[Multi_Map[A, B1]]) {
case (m1, (a, bs)) => (bs :\ m1) { case (b, m2) => m2.insert(a, b) }
}