src/Pure/General/path.scala

--- a/src/Pure/General/path.scala	Wed Mar 03 22:48:46 2021 +0100
+++ b/src/Pure/General/path.scala	Thu Mar 04 15:41:46 2021 +0100
@@ -146,10 +146,10 @@
   def check_case_insensitive(paths: List[Path]): Unit =
   {
     val table =
-      (Multi_Map.empty[String, String] /: paths)({ case (tab, path) =>
+      paths.foldLeft(Multi_Map.empty[String, String]) { case (tab, path) =>
         val name = path.expand.implode
         tab.insert(Word.lowercase(name), name)
-      })
+      }
     val collisions =
       (for { (_, coll) <- table.iterator_list if coll.length > 1 } yield coll).toList.flatten
     if (collisions.nonEmpty) {