# HG changeset patch
# User wenzelm
# Date 1226953726 -3600
# Node ID 3b460b6eadae14a7550a00f7abcd5b9999623712
# Parent  415c7ffeb4cb6108c8041a4d38bdb38b3f0c8d61
simplified thm_deps -- no need to build a graph datastructure;

diff -r 415c7ffeb4cb -r 3b460b6eadae src/Pure/Thy/thm_deps.ML
--- a/src/Pure/Thy/thm_deps.ML	Mon Nov 17 21:13:48 2008 +0100
+++ b/src/Pure/Thy/thm_deps.ML	Mon Nov 17 21:28:46 2008 +0100
@@ -16,36 +16,33 @@
 
 (* thm_deps *)
 
-fun add_dep (name, _, PBody {thms = thms', ...}) =
-  name <> "" ?
-    Graph.new_node (name, ()) #>
-    fold (fn (_, (name', _, _)) => name <> "" ? Graph.add_edge (name', name)) thms';
-
 fun thm_deps thms =
   let
-    val graph = Proofterm.fold_body_thms add_dep (map Thm.proof_body_of thms) Graph.empty;
-    fun add_entry (name, (_, (preds, _))) =
-      let
-        val prefix = #1 (Library.split_last (NameSpace.explode name));
-        val session =
-          (case prefix of
-            a :: _ =>
-              (case ThyInfo.lookup_theory a of
-                SOME thy =>
-                  (case Present.session_name thy of
-                    "" => []
-                  | session => [session])
-              | NONE => [])
-           | _ => ["global"]);
-        val entry =
-          {name = Sign.base_name name,
-           ID = name,
-           dir = space_implode "/" (session @ prefix),
-           unfold = false,
-           path = "",
-           parents = preds};
-      in cons entry end;
-  in Present.display_graph (sort_wrt #ID (Graph.fold add_entry graph [])) end;
+    fun add_dep ("", _, _) = I
+      | add_dep (name, _, PBody {thms = thms', ...}) =
+          let
+            val prefix = #1 (Library.split_last (NameSpace.explode name));
+            val session =
+              (case prefix of
+                a :: _ =>
+                  (case ThyInfo.lookup_theory a of
+                    SOME thy =>
+                      (case Present.session_name thy of
+                        "" => []
+                      | session => [session])
+                  | NONE => [])
+               | _ => ["global"]);
+            val parents = filter_out (fn s => s = "") (map (#1 o #2) thms');
+            val entry =
+              {name = Sign.base_name name,
+               ID = name,
+               dir = space_implode "/" (session @ prefix),
+               unfold = false,
+               path = "",
+               parents = parents};
+          in cons entry end;
+    val deps = Proofterm.fold_body_thms add_dep (map Thm.proof_body_of thms) [];
+  in Present.display_graph (sort_wrt #ID deps) end;
 
 
 (* unused_thms *)