# HG changeset patch
# User wenzelm
# Date 1275146762 -7200
# Node ID 64da21a2c6c7a0740f1ad6a0dce49366c9615b82
# Parent  79fe8e753e84a765519ba3fd223a0fbf41664287
avoid :\ which is not tail-recursive and tends to overflow the tiny JVM stack, which is not resizable at runtime;

diff -r 79fe8e753e84 -r 64da21a2c6c7 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] =
   {