# HG changeset patch
# User wenzelm
# Date 1330112272 -3600
# Node ID f114004247829ca4ab4237c3e5fd964a4b17e0d5
# Parent  61aac9bd43fab2d951c77a7edb15badb928e49f7
discontinued obsolete Graph.all_paths (last seen in 1524d69783d3 and AFP/80bbbdbfec62);

diff -r 61aac9bd43fa -r f11400424782 src/Pure/General/graph.ML
--- a/src/Pure/General/graph.ML	Fri Feb 24 19:47:11 2012 +0100
+++ b/src/Pure/General/graph.ML	Fri Feb 24 20:37:52 2012 +0100
@@ -53,7 +53,6 @@
   val join: (key -> 'a * 'a -> 'a) (*exception DUP/SAME*) ->
     'a T * 'a T -> 'a T                                               (*exception DUP*)
   val irreducible_paths: 'a T -> key * key -> key list list
-  val all_paths: 'a T -> key * key -> key list list
   exception CYCLES of key list list
   val add_edge_acyclic: key * key -> 'a T -> 'a T                     (*exception UNDEF | CYCLES*)
   val add_deps_acyclic: key * key list -> 'a T -> 'a T                (*exception UNDEF | CYCLES*)
@@ -270,19 +269,6 @@
   in if eq_key (x, y) andalso not (is_edge G (x, x)) then [[]] else paths [] y [] end;
 
 
-(* all paths *)
-
-fun all_paths G (x, y) =
-  let
-    val (_, X) = reachable (imm_succs G) [x];
-    fun paths path z =
-      if not (null path) andalso eq_key (x, z) then [z :: path]
-      else if Keys.member X z andalso not (member eq_key path z)
-      then maps (paths (z :: path)) (immediate_preds G z)
-      else [];
-  in paths [] y end;
-
-
 (* maintain acyclic graphs *)
 
 exception CYCLES of key list list;