1.1 --- a/src/Pure/General/graph.ML	Fri Feb 24 19:47:11 2012 +0100
     1.2 +++ b/src/Pure/General/graph.ML	Fri Feb 24 20:37:52 2012 +0100
     1.3 @@ -53,7 +53,6 @@
     1.4    val join: (key -> 'a * 'a -> 'a) (*exception DUP/SAME*) ->
     1.5      'a T * 'a T -> 'a T                                               (*exception DUP*)
     1.6    val irreducible_paths: 'a T -> key * key -> key list list
     1.7 -  val all_paths: 'a T -> key * key -> key list list
     1.8    exception CYCLES of key list list
     1.9    val add_edge_acyclic: key * key -> 'a T -> 'a T                     (*exception UNDEF | CYCLES*)
    1.10    val add_deps_acyclic: key * key list -> 'a T -> 'a T                (*exception UNDEF | CYCLES*)
    1.11 @@ -270,19 +269,6 @@
    1.12    in if eq_key (x, y) andalso not (is_edge G (x, x)) then [[]] else paths [] y [] end;
    1.13  
    1.14  
    1.15 -(* all paths *)
    1.16 -
    1.17 -fun all_paths G (x, y) =
    1.18 -  let
    1.19 -    val (_, X) = reachable (imm_succs G) [x];
    1.20 -    fun paths path z =
    1.21 -      if not (null path) andalso eq_key (x, z) then [z :: path]
    1.22 -      else if Keys.member X z andalso not (member eq_key path z)
    1.23 -      then maps (paths (z :: path)) (immediate_preds G z)
    1.24 -      else [];
    1.25 -  in paths [] y end;
    1.26 -
    1.27 -
    1.28  (* maintain acyclic graphs *)
    1.29  
    1.30  exception CYCLES of key list list;