src/Pure/General/path.scala

--- a/src/Pure/General/path.scala	Thu Mar 04 15:49:15 2021 +0100
+++ b/src/Pure/General/path.scala	Thu Mar 04 15:52:08 2021 +0100
@@ -54,7 +54,7 @@
     }
 
   private def norm_elems(elems: List[Elem]): List[Elem] =
-    elems.foldRight(Nil: List[Elem])(apply_elem)
+    elems.foldRight(List.empty[Elem])(apply_elem)
 
   private def implode_elem(elem: Elem, short: Boolean): String =
     elem match {