tuned;

--- 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()
       }
   }
 

--- a/src/Pure/library.scala	Sun Aug 22 20:25:15 2010 +0200
+++ b/src/Pure/library.scala	Sun Aug 22 22:09:14 2010 +0200
@@ -79,7 +79,7 @@
     def next(): CharSequence =
       state match {
         case Some((s, i)) => { state = next_chunk(i); s }
-        case None => throw new NoSuchElementException("next on empty iterator")
+        case None => Iterator.empty.next()
       }
   }