| changeset 21926 | 1091904ddb19 |
| parent 20573 | c945a208e7f8 |
| child 21933 | 819ef284720b |
--- 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;