# HG changeset patch
# User wenzelm
# Date 964347041 -7200
# Node ID c4f7c959eaee692ea8dc63f56dd447cd0cd62fd9
# Parent  9144976964e76e39e8047a8ef7b42916ba5e4dfe
get_names: topologically sorted;

diff -r 9144976964e7 -r c4f7c959eaee src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Sun Jul 23 12:10:11 2000 +0200
+++ b/src/Pure/Thy/thy_info.ML	Sun Jul 23 12:10:41 2000 +0200
@@ -119,7 +119,11 @@
 (* access thy graph *)
 
 fun thy_graph f x = f (get_thys ()) x;
-fun get_names () = Graph.keys (get_thys ());
+
+(*theory names in topological order*)
+fun get_names () =
+  let val G = get_thys ()
+  in Graph.all_succs G (filter (Library.null o Graph.imm_preds G) (Graph.keys G)) end;
 
 
 (* access thy *)