src/Pure/General/linear_set.scala

--- a/src/Pure/General/linear_set.scala	Sat May 29 16:44:44 2010 +0200
+++ b/src/Pure/General/linear_set.scala	Sat May 29 17:26:02 2010 +0200
@@ -103,7 +103,9 @@
     }
 
   def append_after(hook: Option[A], elems: Seq[A]): Linear_Set[A] =
-    (elems :\ this)((elem, set) => set.insert_after(hook, elem))
+    ((hook, this) /: elems) {
+      case ((last_elem, set), elem) => (Some(elem), set.insert_after(last_elem, elem))
+    }._2
 
   def delete_between(from: Option[A], to: Option[A]): Linear_Set[A] =
   {