# HG changeset patch
# User wenzelm
# Date 1679946796 -7200
# Node ID b4032c468d7495dccec601851496f5ab91095d4c
# Parent  b761c91c2447daf0758db5559bee97dda79faac5
performanc tuning: avoid exception overhead, potentially relevant for Sorts.class_less;

diff -r b761c91c2447 -r b4032c468d74 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