src/Pure/General/scan.scala

--- a/src/Pure/General/scan.scala	Thu Mar 04 15:52:08 2021 +0100
+++ b/src/Pure/General/scan.scala	Thu Mar 04 15:59:28 2021 +0100
@@ -390,7 +390,8 @@
         new Lexicon(extend(rep, 0))
       }
 
-    def ++ (elems: IterableOnce[String]): Lexicon = elems.foldLeft(this)(_ + _)
+    def ++ (elems: IterableOnce[String]): Lexicon =
+      elems.iterator.foldLeft(this)(_ + _)
 
     def ++ (other: Lexicon): Lexicon =
       if (this eq other) this