--- a/src/Pure/General/linear_set.scala Thu Mar 04 15:52:08 2021 +0100
+++ b/src/Pure/General/linear_set.scala Thu Mar 04 15:59:28 2021 +0100
@@ -18,7 +18,8 @@
private val empty_val: Linear_Set[Nothing] = new Linear_Set[Nothing](None, None, Map(), Map())
override def empty[A]: Linear_Set[A] = empty_val.asInstanceOf[Linear_Set[A]]
- def from[A](entries: IterableOnce[A]): Linear_Set[A] = entries.foldLeft(empty[A])(_.incl(_))
+ def from[A](entries: IterableOnce[A]): Linear_Set[A] =
+ entries.iterator.foldLeft(empty[A])(_.incl(_))
override def newBuilder[A]: mutable.Builder[A, Linear_Set[A]] = new Builder[A]
private class Builder[A] extends mutable.Builder[A, Linear_Set[A]]