# HG changeset patch
# User wenzelm
# Date 1344597300 -7200
# Node ID 5e57a6f24cdb3bd613609a9b7634829c18e30c69
# Parent  8a81ef0bc79002bf8d077fa6e91f85596f1f5e7f
tuned;

diff -r 8a81ef0bc790 -r 5e57a6f24cdb src/Pure/General/linear_set.scala
--- a/src/Pure/General/linear_set.scala	Fri Aug 10 10:23:54 2012 +0200
+++ b/src/Pure/General/linear_set.scala	Fri Aug 10 13:15:00 2012 +0200
@@ -34,8 +34,6 @@
 {
   override def companion: GenericCompanion[Linear_Set] = Linear_Set
 
-  def reverse: Linear_Set[A] = new Linear_Set(end, start, prevs, nexts)
-
 
   /* relative addressing */
 
@@ -76,7 +74,7 @@
             }
       }
 
-  def append_after(hook: Option[A], elems: Seq[A]): Linear_Set[A] =
+  def append_after(hook: Option[A], elems: Seq[A]): Linear_Set[A] =  // FIXME reverse fold
     ((hook, this) /: elems) {
       case ((last, set), elem) => (Some(elem), set.insert_after(last, elem))
     }._2
@@ -147,6 +145,10 @@
         case Some(stop) => iterator(from).takeWhile(_ != stop)
       }
 
+  def reverse: Linear_Set[A] = new Linear_Set(end, start, prevs, nexts)
+
+  override def last: A = reverse.head
+
   def + (elem: A): Linear_Set[A] = insert_after(end, elem)
 
   def - (elem: A): Linear_Set[A] =