performanc tuning: avoid exception overhead, potentially relevant for Sorts.class_less;
authorwenzelm
Mon, 27 Mar 2023 21:53:16 +0200
changeset 77724 b4032c468d74
parent 77723 b761c91c2447
child 77725 96a594e5e054
performanc tuning: avoid exception overhead, potentially relevant for Sorts.class_less;
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