src/Pure/Thy/thm_deps.ML
changeset 28826 3b460b6eadae
parent 28817 c8cc94a470d4
child 29606 fedb8be05f24
     1.1 --- a/src/Pure/Thy/thm_deps.ML	Mon Nov 17 21:13:48 2008 +0100
     1.2 +++ b/src/Pure/Thy/thm_deps.ML	Mon Nov 17 21:28:46 2008 +0100
     1.3 @@ -16,36 +16,33 @@
     1.4  
     1.5  (* thm_deps *)
     1.6  
     1.7 -fun add_dep (name, _, PBody {thms = thms', ...}) =
     1.8 -  name <> "" ?
     1.9 -    Graph.new_node (name, ()) #>
    1.10 -    fold (fn (_, (name', _, _)) => name <> "" ? Graph.add_edge (name', name)) thms';
    1.11 -
    1.12  fun thm_deps thms =
    1.13    let
    1.14 -    val graph = Proofterm.fold_body_thms add_dep (map Thm.proof_body_of thms) Graph.empty;
    1.15 -    fun add_entry (name, (_, (preds, _))) =
    1.16 -      let
    1.17 -        val prefix = #1 (Library.split_last (NameSpace.explode name));
    1.18 -        val session =
    1.19 -          (case prefix of
    1.20 -            a :: _ =>
    1.21 -              (case ThyInfo.lookup_theory a of
    1.22 -                SOME thy =>
    1.23 -                  (case Present.session_name thy of
    1.24 -                    "" => []
    1.25 -                  | session => [session])
    1.26 -              | NONE => [])
    1.27 -           | _ => ["global"]);
    1.28 -        val entry =
    1.29 -          {name = Sign.base_name name,
    1.30 -           ID = name,
    1.31 -           dir = space_implode "/" (session @ prefix),
    1.32 -           unfold = false,
    1.33 -           path = "",
    1.34 -           parents = preds};
    1.35 -      in cons entry end;
    1.36 -  in Present.display_graph (sort_wrt #ID (Graph.fold add_entry graph [])) end;
    1.37 +    fun add_dep ("", _, _) = I
    1.38 +      | add_dep (name, _, PBody {thms = thms', ...}) =
    1.39 +          let
    1.40 +            val prefix = #1 (Library.split_last (NameSpace.explode name));
    1.41 +            val session =
    1.42 +              (case prefix of
    1.43 +                a :: _ =>
    1.44 +                  (case ThyInfo.lookup_theory a of
    1.45 +                    SOME thy =>
    1.46 +                      (case Present.session_name thy of
    1.47 +                        "" => []
    1.48 +                      | session => [session])
    1.49 +                  | NONE => [])
    1.50 +               | _ => ["global"]);
    1.51 +            val parents = filter_out (fn s => s = "") (map (#1 o #2) thms');
    1.52 +            val entry =
    1.53 +              {name = Sign.base_name name,
    1.54 +               ID = name,
    1.55 +               dir = space_implode "/" (session @ prefix),
    1.56 +               unfold = false,
    1.57 +               path = "",
    1.58 +               parents = parents};
    1.59 +          in cons entry end;
    1.60 +    val deps = Proofterm.fold_body_thms add_dep (map Thm.proof_body_of thms) [];
    1.61 +  in Present.display_graph (sort_wrt #ID deps) end;
    1.62  
    1.63  
    1.64  (* unused_thms *)