src/Pure/General/linear_set.scala
changeset 65374 ce09e947c1d5
parent 64370 865b39487b5d
     1.1 --- a/src/Pure/General/linear_set.scala	Tue Apr 04 18:43:47 2017 +0200
     1.2 +++ b/src/Pure/General/linear_set.scala	Tue Apr 04 18:43:58 2017 +0200
     1.3 @@ -78,7 +78,7 @@
     1.4              }
     1.5        }
     1.6  
     1.7 -  def append_after(hook: Option[A], elems: Seq[A]): Linear_Set[A] =  // FIXME reverse fold
     1.8 +  def append_after(hook: Option[A], elems: Traversable[A]): Linear_Set[A] =  // FIXME reverse fold
     1.9      ((hook, this) /: elems) {
    1.10        case ((last, set), elem) => (Some(elem), set.insert_after(last, elem))
    1.11      }._2