# HG changeset patch
# User wenzelm
# Date 1175722182 -7200
# Node ID a165d9ed08b8df31bd0f7421740b78e94176a6c9
# Parent  948f23d4af290dd2dbf3f596848898f18812c56f
simplified thy_deps using Theory.ancestors_of (in order of creation);

diff -r 948f23d4af29 -r a165d9ed08b8 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Wed Apr 04 23:29:41 2007 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Wed Apr 04 23:29:42 2007 +0200
@@ -494,12 +494,12 @@
 val thy_deps = Toplevel.unknown_theory o Toplevel.keep (fn state =>
   let
     val thy = Toplevel.theory_of state;
-    val gr = Theory.dep_graph thy;
-    fun mk_entry (name, ((), (_, parents))) =
-      { name = name, ID = name, dir = "", unfold = true,
-        path = "", parents = parents };
-    val prgr = Graph.fold ((fn x => fn xs => xs @ [x]) o mk_entry) gr [];
-  in Present.display_graph prgr end);
+    val gr = rev (thy :: Theory.ancestors_of thy) |> map (fn node =>
+      let
+        val name = Context.theory_name node;
+        val parents = map Context.theory_name (Theory.parents_of node);
+      in {name = name, ID = name, parents = parents, dir = "", unfold = true, path = ""} end);
+  in Present.display_graph gr end);
 
 val class_deps = Toplevel.unknown_theory o Toplevel.keep (fn state =>
   let