diff -r ef8c9b3d5355 -r dde25151c3c1 src/Pure/General/linear_set.scala
--- 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]]