# HG changeset patch
# User haftmann
# Date 1167390663 -3600
# Node ID 1091904ddb19dcfde07635bbb2b1987c5bb25ef5
# Parent  5389dcd524e3020c3f9889c43d56536b45d4ead1
``classes`` now returns classes in topological order

diff -r 5389dcd524e3 -r 1091904ddb19 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;