1.1 --- a/src/Pure/General/graph.scala	Wed Jul 25 23:02:50 2012 +0200
     1.2 +++ b/src/Pure/General/graph.scala	Thu Jul 26 11:46:30 2012 +0200
     1.3 @@ -39,6 +39,7 @@
     1.4    /* graphs */
     1.5  
     1.6    def is_empty: Boolean = rep.isEmpty
     1.7 +  def defined(x: Key): Boolean = rep.isDefinedAt(x)
     1.8  
     1.9    def entries: Iterator[(Key, Entry)] = rep.iterator
    1.10    def keys: Iterator[Key] = entries.map(_._1)
    1.11 @@ -155,8 +156,7 @@
    1.12    /* edge operations */
    1.13  
    1.14    def is_edge(x: Key, y: Key): Boolean =
    1.15 -    try { imm_succs(x)(y) }
    1.16 -    catch { case _: Graph.Undefined[_] => false }
    1.17 +    defined(x) && defined(y) && imm_succs(x)(y)
    1.18  
    1.19    def add_edge(x: Key, y: Key): Graph[Key, A] =
    1.20      if (is_edge(x, y)) this