| changeset 46712 | 8650d9a95736 |
| parent 46668 | 9034b44844bd |
| child 48348 | cbb25adad26f |
--- a/src/Pure/General/graph.scala Mon Feb 27 16:56:25 2012 +0100 +++ b/src/Pure/General/graph.scala Mon Feb 27 17:13:25 2012 +0100 @@ -27,7 +27,7 @@ } -class Graph[Key, A] private(rep: SortedMap[Key, (A, (SortedSet[Key], SortedSet[Key]))]) +final class Graph[Key, A] private(rep: SortedMap[Key, (A, (SortedSet[Key], SortedSet[Key]))]) { type Keys = SortedSet[Key] type Entry = (A, (Keys, Keys))