get_names: topologically sorted;

--- 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 *)