# HG changeset patch
# User wenzelm
# Date 1330017298 -3600
# Node ID 9aea30f3b954ad7bdac5e1456ff8b09d32dedce8
# Parent  08cb66dc7d2cb81f08b4a84ac6f7e81eb23eba71
tuned;

diff -r 08cb66dc7d2c -r 9aea30f3b954 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 {