diff -r ef8c9b3d5355 -r dde25151c3c1 src/Pure/General/multi_map.scala --- a/src/Pure/General/multi_map.scala Thu Mar 04 15:52:08 2021 +0100 +++ b/src/Pure/General/multi_map.scala Thu Mar 04 15:59:28 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] = - entries.foldLeft(empty[A, B]) { case (m, (a, b)) => m.insert(a, b) } + entries.iterator.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]]