improved add_edges_cyclic;

--- 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);