diff -r 1cd71fb32831 -r 3b9eede40608 src/Pure/Thy/thm_deps.ML
--- a/src/Pure/Thy/thm_deps.ML	Wed Apr 16 21:53:04 2008 +0200
+++ b/src/Pure/Thy/thm_deps.ML	Wed Apr 16 21:53:05 2008 +0200
@@ -5,27 +5,26 @@
 Visualize dependencies of theorems.
 *)
 
-signature BASIC_THM_DEPS =
-sig
-  val thm_deps : thm list -> unit
-end;
-
 signature THM_DEPS =
 sig
-  include BASIC_THM_DEPS
-  val enable : unit -> unit
-  val disable : unit -> unit
-  val unused_thms : theory list option * theory list -> (string * thm) list
+  val enable: unit -> unit
+  val disable: unit -> unit
+  val thm_deps: thm list -> unit
+  val unused_thms: theory list * theory list -> (string * thm) list
 end;
 
-structure ThmDeps : THM_DEPS =
+structure ThmDeps: THM_DEPS =
 struct
 
+(* thm_deps *)
+
+fun enable () = CRITICAL (fn () => if ! proofs = 0 then proofs := 1 else ());
+fun disable () = proofs := 0;
+
+local
+
 open Proofterm;
 
-fun enable () = if ! proofs = 0 then proofs := 1 else ();
-fun disable () = proofs := 0;
-
 fun dest_thm_axm (PThm (name, prf, _, _)) = (name, prf)
   | dest_thm_axm (PAxm (name, _, _)) = (name ^ " (Ax)", MinProof ([], [], []))
   | dest_thm_axm _ = ("", MinProof ([], [], []));
@@ -67,45 +66,47 @@
           make_deps_graph prf' (gra, parents)
       end);
 
+in
+
 fun thm_deps thms =
   Present.display_graph
     (map snd (sort_wrt fst (Symtab.dest (fst
       (fold make_deps_graph (map Thm.proof_of thms) (Symtab.empty, []))))));
 
-fun unused_thms (opt_thys1, thys2) =
+end;
+
+
+(* unused_thms *)
+
+fun unused_thms (base_thys, thys) =
   let
-    val thys = case opt_thys1 of
-        NONE => thys2
-      | SOME thys1 =>
-          thys2 |>
-          fold (curry (gen_union Theory.eq_thy)) (map Context.ancestors_of thys2) |>
-          fold (subtract Theory.eq_thy) (thys1 :: map Context.ancestors_of thys1);
-    val thms = maps PureThy.thms_of thys;
+    fun add_fact (name, ths) =
+      if exists (fn thy => PureThy.defined_fact thy name) base_thys then I
+      else fold_rev (fn th => (case Thm.get_name th of "" => I | a => cons (a, th))) ths;
+    val thms = sort_wrt #1 (fold (Facts.fold_static add_fact o PureThy.facts_of) thys []);
     val tab = fold Proofterm.thms_of_proof
-      (map (Proofterm.strip_thm o proof_of o snd) thms) Symtab.empty;
-    fun is_unused (s, thm) = case Symtab.lookup tab s of
+      (map (Proofterm.strip_thm o Thm.proof_of o snd) thms) Symtab.empty;
+    fun is_unused (name, th) = case Symtab.lookup tab name of
         NONE => true
-      | SOME ps => not (prop_of thm mem map fst ps);
+      | SOME ps => not (member (op aconv) (map fst ps) (Thm.prop_of th));
     (* groups containing at least one used theorem *)
     val grps = fold (fn p as (_, thm) => if is_unused p then I else
       case PureThy.get_group thm of
         NONE => I | SOME grp => Symtab.update (grp, ())) thms Symtab.empty;
     val (thms', _) = fold (fn p as (s, thm) => fn q as (thms, grps') =>
-      if PureThy.get_kind thm mem [Thm.theoremK, Thm.lemmaK, Thm.corollaryK, Thm.axiomK]
+      if member (op =) [Thm.theoremK, Thm.lemmaK, Thm.corollaryK, Thm.axiomK] (PureThy.get_kind thm)
         andalso is_unused p
       then
         (case PureThy.get_group thm of
            NONE => (p :: thms, grps')
          | SOME grp =>
              (* do not output theorem if another theorem in group has been used *)
-             if is_some (Symtab.lookup grps grp) then q
+             if Symtab.defined grps grp then q
              (* output at most one unused theorem per group *)
-             else if is_some (Symtab.lookup grps' grp) then q
+             else if Symtab.defined grps' grp then q
              else (p :: thms, Symtab.update (grp, ()) grps'))
       else q) thms ([], Symtab.empty)
   in rev thms' end;
 
 end;
 
-structure BasicThmDeps : BASIC_THM_DEPS = ThmDeps;
-open BasicThmDeps;