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