diff -r 3a6ce43d99b1 -r ff7f9510b0d6 src/Pure/General/linear_set.scala
--- a/src/Pure/General/linear_set.scala	Sun Aug 22 20:25:15 2010 +0200
+++ b/src/Pure/General/linear_set.scala	Sun Aug 22 22:09:14 2010 +0200
@@ -143,13 +143,13 @@
 
   private def make_iterator(start: Option[A], which: Map[A, A]): Iterator[A] = new Iterator[A] {
     private var next_elem = start
-    def hasNext = next_elem.isDefined
-    def next =
+    def hasNext(): Boolean = next_elem.isDefined
+    def next(): A =
       next_elem match {
         case Some(elem) =>
           next_elem = which.get(elem)
           elem
-        case None => throw new NoSuchElementException("next on empty iterator")
+        case None => Iterator.empty.next()
       }
   }