# HG changeset patch
# User wenzelm
# Date 1203965286 -3600
# Node ID dc578de1d3e925668aa6cc8c3d6bc74bb5c0d894
# Parent  9b47c8a2d869908697f6e3a7d495ded336f7dfdb
thm_deps: sort result;

diff -r 9b47c8a2d869 -r dc578de1d3e9 src/Pure/Thy/thm_deps.ML
--- a/src/Pure/Thy/thm_deps.ML	Mon Feb 25 19:38:48 2008 +0100
+++ b/src/Pure/Thy/thm_deps.ML	Mon Feb 25 19:48:06 2008 +0100
@@ -68,8 +68,8 @@
 
 fun thm_deps thms =
   Present.display_graph
-    (map snd (Symtab.dest (fst
-      (fold make_deps_graph (map Thm.proof_of thms) (Symtab.empty, [])))));
+    (map snd (sort_wrt fst (Symtab.dest (fst
+      (fold make_deps_graph (map Thm.proof_of thms) (Symtab.empty, []))))));
 
 end;