# HG changeset patch
# User berghofe
# Date 1007995023 -3600
# Node ID 0224f472be7134057d6732d78c9d0b2ffe5c0cac
# Parent  1162b280700a4af087a9bc55bd1218bd97315768
Fixed bug in function find_paths.

diff -r 1162b280700a -r 0224f472be71 src/Pure/General/graph.ML
--- a/src/Pure/General/graph.ML	Mon Dec 10 15:36:05 2001 +0100
+++ b/src/Pure/General/graph.ML	Mon Dec 10 15:37:03 2001 +0100
@@ -124,10 +124,11 @@
   let
     val (_, X) = reachable (imm_succs G) [x];
     fun paths ps p =
-      if eq_key (p, x) then [p :: ps]
-      else flat (map (paths (p :: ps))
-        (filter (fn pp => pp mem_keys X andalso not (pp mem_key ps)) (imm_preds G p)));
-  in get_entry G y; if y mem_keys X then (paths [] y) else [] end;
+      if not (null ps) andalso eq_key (p, x) then [p :: ps]
+      else if p mem_keys X andalso not (p mem_key ps)
+      then flat (map (paths (p :: ps)) (imm_preds G p))
+      else [];
+  in paths [] y end;
 
 
 (* nodes *)