# HG changeset patch
# User wenzelm
# Date 1253052772 -7200
# Node ID 892ebdaf19b4cbce11147ea2b43ec1c7a96c7474
# Parent  20b261654e33413afef0055c01cda8e0ca4c05bb
added append_after (tuned version of former insert_after of Seq);

diff -r 20b261654e33 -r 892ebdaf19b4 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