performanc tuning: avoid exception overhead, potentially relevant for Sorts.class_less;
--- 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