src/Pure/General/graph.ML

--- a/src/Pure/General/graph.ML	Mon Mar 27 21:48:47 2023 +0200
+++ b/src/Pure/General/graph.ML	Mon Mar 27 21:53:16 2023 +0200
@@ -208,7 +208,10 @@
 
 (* edge operations *)
 
-fun is_edge G (x, y) = Keys.member (imm_succs G x) y handle UNDEF _ => false;
+fun is_edge (Graph tab) (x, y) =
+  (case Table.lookup tab x of
+    SOME (_, (_, succs)) => Keys.member succs y
+  | NONE => false);
 
 fun add_edge (x, y) G =
   if is_edge G (x, y) then G