# HG changeset patch
# User wenzelm
# Date 1253129517 -7200
# Node ID 9433e7435b9b6f02783b8085a8ac8b74735618b8
# Parent  95f4f08f950f79073205ba8fc4086d775b6844bf
tuned;

diff -r 95f4f08f950f -r 9433e7435b9b src/Pure/General/linear_set.scala
--- a/src/Pure/General/linear_set.scala	Wed Sep 16 21:14:08 2009 +0200
+++ b/src/Pure/General/linear_set.scala	Wed Sep 16 21:31:57 2009 +0200
@@ -93,11 +93,11 @@
     }
 
   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))
+    (elems :\ this)((elem, set) => set.insert_after(hook, elem))
 
   def delete_between(from: Option[A], to: Option[A]): Linear_Set[A] =
   {
-    if (!rep.first.isDefined) this
+    if (isEmpty) this
     else {
       val next =
         if (from == rep.last) None
@@ -123,7 +123,7 @@
     def hasNext = next_elem.isDefined
     def next = {
       val elem = next_elem.get
-      next_elem = if (rep.nexts.isDefinedAt(elem)) Some(rep.nexts(elem)) else None
+      next_elem = rep.nexts.get(elem)
       elem
     }
   }