diff -r af1dabad14c0 -r 1182677e4728 src/Pure/General/graph.scala
--- a/src/Pure/General/graph.scala	Wed Jul 25 23:02:50 2012 +0200
+++ b/src/Pure/General/graph.scala	Thu Jul 26 11:46:30 2012 +0200
@@ -39,6 +39,7 @@
   /* graphs */
 
   def is_empty: Boolean = rep.isEmpty
+  def defined(x: Key): Boolean = rep.isDefinedAt(x)
 
   def entries: Iterator[(Key, Entry)] = rep.iterator
   def keys: Iterator[Key] = entries.map(_._1)
@@ -155,8 +156,7 @@
   /* edge operations */
 
   def is_edge(x: Key, y: Key): Boolean =
-    try { imm_succs(x)(y) }
-    catch { case _: Graph.Undefined[_] => false }
+    defined(x) && defined(y) && imm_succs(x)(y)
 
   def add_edge(x: Key, y: Key): Graph[Key, A] =
     if (is_edge(x, y)) this