``classes`` now returns classes in topological order
authorhaftmann
Fri, 29 Dec 2006 12:11:03 +0100
changeset 21926 1091904ddb19
parent 21925 5389dcd524e3
child 21927 9677abe5d374
``classes`` now returns classes in topological order
src/Pure/sorts.ML
--- a/src/Pure/sorts.ML	Fri Dec 29 12:11:02 2006 +0100
+++ b/src/Pure/sorts.ML	Fri Dec 29 12:11:03 2006 +0100
@@ -120,7 +120,8 @@
 
 (* classes *)
 
-val classes = Graph.keys o classes_of;
+val classes = flat o rev o Graph.strong_conn o classes_of;
+  (*order allows for left-to-right traversal*)
 val super_classes = Graph.imm_succs o classes_of;