| changeset 67018 | f6aa133f9b16 |
| parent 67012 | 671decd2e627 |
| child 67935 | 61888dd27f73 |
--- a/src/Pure/General/graph.scala Tue Nov 07 10:22:10 2017 +0100 +++ b/src/Pure/General/graph.scala Tue Nov 07 11:11:37 2017 +0100 @@ -70,7 +70,6 @@ def keys_iterator: Iterator[Key] = iterator.map(_._1) def keys: List[Key] = keys_iterator.toList - def keys_set: Set[Key] = rep.keySet def dest: List[((Key, A), List[Key])] = (for ((x, (i, (_, succs))) <- iterator) yield ((x, i), succs.toList)).toList