src/Pure/General/linear_set.scala

--- a/src/Pure/General/linear_set.scala	Thu Feb 23 17:27:37 2012 +0100
+++ b/src/Pure/General/linear_set.scala	Thu Feb 23 18:14:58 2012 +0100
@@ -141,8 +141,8 @@
   def contains(elem: A): Boolean =
     !isEmpty && (rep.end.get == elem || rep.nexts.isDefinedAt(elem))
 
-  private def make_iterator(start: Option[A], which: Map[A, A]): Iterator[A] = new Iterator[A] {
-    private var next_elem = start
+  private def make_iterator(from: Option[A], which: Map[A, A]): Iterator[A] = new Iterator[A] {
+    private var next_elem = from
     def hasNext(): Boolean = next_elem.isDefined
     def next(): A =
       next_elem match {