# HG changeset patch
# User wenzelm
# Date 1185299076 -7200
# Node ID d2df2797519bcb78204c47637f25344f612d5ad2
# Parent  c2ee97a963db65598fb82c17fc4e7fb8b30d9c99
added topological_order;
tuned;

diff -r c2ee97a963db -r d2df2797519b src/Pure/General/graph.ML
--- a/src/Pure/General/graph.ML	Tue Jul 24 19:44:35 2007 +0200
+++ b/src/Pure/General/graph.ML	Tue Jul 24 19:44:36 2007 +0200
@@ -44,6 +44,7 @@
   val add_edge_acyclic: key * key -> 'a T -> 'a T                     (*exception CYCLES*)
   val add_deps_acyclic: key * key list -> 'a T -> 'a T                (*exception CYCLES*)
   val merge_acyclic: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T         (*exception CYCLES*)
+  val topological_order: 'a T -> key list
   val add_edge_trans_acyclic: key * key -> 'a T -> 'a T               (*exception CYCLES*)
   val merge_trans_acyclic: ('a * 'a -> bool) -> 'a T * 'a T -> 'a T   (*exception CYCLES*)
 end;
@@ -130,7 +131,7 @@
     fun reach x (rs, R) =
       if member_keys R x then (rs, R)
       else apfst (cons x) (fold reach (next x) (rs, insert_keys x R))
-  in fold_map (fn x => reach x o pair []) xs empty_keys end;
+  in fold_map (fn x => fn X => reach x ([], X)) xs empty_keys end;
 
 (*immediate*)
 fun imm_preds G = #1 o #2 o get_entry G;
@@ -249,6 +250,8 @@
 
 fun merge_acyclic eq GG = gen_merge add_edge_acyclic eq GG;
 
+fun topological_order G = minimals G |> all_succs G;
+
 
 (* maintain transitive acyclic graphs *)