# HG changeset patch
# User wenzelm
# Date 963589796 -7200
# Node ID 1791a62b33e714bc85b9ef807dabe7630a78c127
# Parent  297dcbf64526488307d1a8ada6833cddf6260b70
improved add_edges_cyclic;

diff -r 297dcbf64526 -r 1791a62b33e7 src/Pure/General/graph.ML
--- a/src/Pure/General/graph.ML	Fri Jul 14 16:32:51 2000 +0200
+++ b/src/Pure/General/graph.ML	Fri Jul 14 17:49:56 2000 +0200
@@ -162,9 +162,11 @@
 exception CYCLES of key list list;
 
 fun add_edge_acyclic (x, y) G =
-  (case find_paths G (y, x) of
-    [] => add_edge (x, y) G
-  | cycles => raise CYCLES (map (cons x) cycles));
+  if y mem_key imm_succs G x then G
+  else
+    (case find_paths G (y, x) of
+      [] => add_edge (x, y) G
+    | cycles => raise CYCLES (map (cons x) cycles));
 
 fun add_deps_acyclic (y, xs) G =
   foldl (fn (H, x) => add_edge_acyclic (x, y) H) (G, xs);