src/Pure/General/linear_set.scala

--- a/src/Pure/General/linear_set.scala	Sat Jan 09 23:22:56 2010 +0100
+++ b/src/Pure/General/linear_set.scala	Sun Jan 10 17:29:09 2010 +0100
@@ -118,14 +118,16 @@
   override def isEmpty: Boolean = !rep.first.isDefined
   def size: Int = if (isEmpty) 0 else rep.nexts.size + 1
 
-  def elements = new Iterator[A] {
+  def elements: Iterator[A] = new Iterator[A] {
     private var next_elem = rep.first
     def hasNext = next_elem.isDefined
-    def next = {
-      val elem = next_elem.get
-      next_elem = rep.nexts.get(elem)
-      elem
-    }
+    def next =
+      next_elem match {
+        case Some(elem) =>
+          next_elem = rep.nexts.get(elem)
+          elem
+        case None => throw new NoSuchElementException("next on empty iterator")
+      }
   }
 
   def contains(elem: A): Boolean =