| changeset 37072 | 9105c8237c7a |
| parent 37070 | e8906d992b69 |
| child 37185 | 64da21a2c6c7 |
--- a/src/Pure/General/linear_set.scala Sat May 22 23:59:09 2010 +0200 +++ b/src/Pure/General/linear_set.scala Mon May 24 23:01:51 2010 +0200 @@ -147,7 +147,7 @@ if (contains(elem)) make_iterator(Some(elem), rep.nexts) else throw new Linear_Set.Undefined(elem.toString) - def rev_iterator(elem: A): Iterator[A] = + def reverse_iterator(elem: A): Iterator[A] = if (contains(elem)) make_iterator(Some(elem), rep.prevs) else throw new Linear_Set.Undefined(elem.toString)