src/Pure/General/position.scala

       }
   }
 
   object Range
   {
-    def apply(range: Text.Range): T = Offset(range.start) ++ Offset(range.stop)
+    def apply(range: Text.Range): T = Offset(range.start) ::: Offset(range.stop)
     def unapply(pos: T): Option[Text.Range] =
       (pos, pos) match {
         case (Offset(start), End_Offset(stop)) if start <= stop => Some(Text.Range(start, stop))
         case (Offset(start), _) => Some(Text.Range(start, start + 1))
         case _ => None