# HG changeset patch
# User wenzelm
# Date 1159384392 -7200
# Node ID 934358468a1b6a28039ddbaca10fe89ef353378f
# Parent  a041bf3c8f2ff5a87e3d625e1043747d83762d48
tuned all_paths;

diff -r a041bf3c8f2f -r 934358468a1b src/Pure/General/graph.ML
--- a/src/Pure/General/graph.ML	Wed Sep 27 21:13:11 2006 +0200
+++ b/src/Pure/General/graph.ML	Wed Sep 27 21:13:12 2006 +0200
@@ -224,15 +224,15 @@
   in if eq_key (x, y) andalso not (is_edge G (x, x)) then [[]] else paths [] y [] end;
 
 
-(* find ALL paths from x to y *)
+(* all paths *)
 
 fun all_paths G (x, y) =
   let
     val (_, X) = reachable (imm_succs G) [x];
-    fun paths ps p =
-      if not (null ps) andalso eq_key (p, x) then [p :: ps]
-      else if member_keys X p andalso not (member_key ps p)
-      then List.concat (map (paths (p :: ps)) (imm_preds G p))
+    fun paths path z =
+      if not (null path) andalso eq_key (x, z) then [z :: path]
+      else if member_keys X z andalso not (member_key path z)
+      then maps (paths (z :: path)) (imm_preds G z)
       else [];
   in paths [] y end;