# HG changeset patch
# User wenzelm
# Date 1256494781 -3600
# Node ID dd6d8d1f70d2bec5397656fd23cebf2491038ec2
# Parent  3012726e99296429b98db4aaed287ce4845d473d
maintain group via name space, not tags;
tuned;

diff -r 3012726e9929 -r dd6d8d1f70d2 src/Pure/Thy/thm_deps.ML
--- a/src/Pure/Thy/thm_deps.ML	Sun Oct 25 19:19:35 2009 +0100
+++ b/src/Pure/Thy/thm_deps.ML	Sun Oct 25 19:19:41 2009 +0100
@@ -48,37 +48,49 @@
 
 fun unused_thms (base_thys, thys) =
   let
-    fun add_fact (name, ths) =
+    fun add_fact space (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;
+      else
+        let val {concealed, group, ...} = Name_Space.the_entry space name in
+          fold_rev (fn th =>
+            (case Thm.get_name th of
+              "" => I
+            | a => cons (a, (th, concealed, group)))) ths
+        end;
+    fun add_facts facts = Facts.fold_static (add_fact (Facts.space_of facts)) facts;
+
     val thms =
-      fold (Facts.fold_static add_fact o PureThy.facts_of) thys []
+      fold (add_facts o PureThy.facts_of) thys []
       |> sort_distinct (string_ord o pairself #1);
 
     val tab =
       Proofterm.fold_body_thms
-        (fn (name, prop, _) => name <> "" ? Symtab.insert_list (op =) (name, prop))
-        (map (Proofterm.strip_thm o Thm.proof_body_of o snd) thms) Symtab.empty;
-    fun is_unused (name, th) =
-      not (member (op aconv) (Symtab.lookup_list tab name) (Thm.prop_of th));
+        (fn (a, prop, _) => a <> "" ? Symtab.insert_list (op =) (a, prop))
+        (map (Proofterm.strip_thm o Thm.proof_body_of o #1 o #2) thms) Symtab.empty;
+
+    fun is_unused (a, th) =
+      not (member (op aconv) (Symtab.lookup_list tab a) (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 Thm.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 member (op =) [Thm.theoremK, Thm.generatedK, Thm.lemmaK, Thm.corollaryK, Thm.axiomK] (Thm.get_kind thm)
-        andalso is_unused p
+    val used_groups = fold (fn (a, (th, _, group)) =>
+      if is_unused (a, th) then I
+      else
+        (case group of
+          NONE => I
+        | SOME grp => Inttab.update (grp, ()))) thms Inttab.empty;
+    val (thms', _) = fold (fn (a, (th, concealed, group)) => fn q as (thms, grps') =>
+      if member (op =) [Thm.theoremK, Thm.generatedK, Thm.lemmaK, Thm.corollaryK, Thm.axiomK]
+        (Thm.get_kind th) andalso not concealed andalso is_unused (a, th)
       then
-        (case Thm.get_group thm of
-           NONE => (p :: thms, grps')
+        (case group of
+           NONE => ((a, th) :: thms, grps')
          | SOME grp =>
              (* do not output theorem if another theorem in group has been used *)
-             if Symtab.defined grps grp then q
+             if Inttab.defined used_groups grp then q
              (* output at most one unused theorem per group *)
-             else if Symtab.defined grps' grp then q
-             else (p :: thms, Symtab.update (grp, ()) grps'))
-      else q) thms ([], Symtab.empty)
+             else if Inttab.defined grps' grp then q
+             else ((a, th) :: thms, Inttab.update (grp, ()) grps'))
+      else q) thms ([], Inttab.empty)
   in rev thms' end;
 
 end;