src/Pure/General/linear_set.scala

--- a/src/Pure/General/linear_set.scala	Tue Sep 15 23:57:07 2009 +0200
+++ b/src/Pure/General/linear_set.scala	Wed Sep 16 00:12:52 2009 +0200
@@ -92,6 +92,9 @@
           }
     }
 
+  def append_after(hook: Option[A], elems: Seq[A]): Linear_Set[A] =
+    (elems :\ this)((elem: A, ls: Linear_Set[A]) => ls.insert_after(hook, elem))
+
   def delete_between(from: Option[A], to: Option[A]): Linear_Set[A] =
   {
     if (!rep.first.isDefined) this