# HG changeset patch
# User wenzelm
# Date 1257450016 -3600
# Node ID fe551dc9d4bd86fc3be69adbdd23e556b3ce2987
# Parent  c7175a18c0905eb1fb0fca33e58c3269164c7b36
scalable version of Named_Thms, using Item_Net;

diff -r c7175a18c090 -r fe551dc9d4bd src/Pure/Tools/named_thms.ML
--- a/src/Pure/Tools/named_thms.ML	Thu Nov 05 17:59:49 2009 +0100
+++ b/src/Pure/Tools/named_thms.ML	Thu Nov 05 20:40:16 2009 +0100
@@ -1,8 +1,7 @@
 (*  Title:      Pure/Tools/named_thms.ML
     Author:     Makarius
 
-Named collections of theorems in canonical order.  Based on naive data
-structures -- not scalable!
+Named collections of theorems in canonical order.
 *)
 
 signature NAMED_THMS =
@@ -20,22 +19,23 @@
 
 structure Data = GenericDataFun
 (
-  type T = thm list;
-  val empty = [];
+  type T = thm Item_Net.T;
+  val empty = Thm.full_rules;
   val extend = I;
-  fun merge _ = Thm.merge_thms;
+  fun merge _ = Item_Net.merge;
 );
 
-val get = Data.get o Context.Proof;
+val content = Item_Net.content o Data.get;
+val get = content o Context.Proof;
 
-val add_thm = Data.map o Thm.add_thm;
-val del_thm = Data.map o Thm.del_thm;
+val add_thm = Data.map o Item_Net.update;
+val del_thm = Data.map o Item_Net.remove;
 
 val add = Thm.declaration_attribute add_thm;
 val del = Thm.declaration_attribute del_thm;
 
 val setup =
   Attrib.setup (Binding.name name) (Attrib.add_del add del) ("declaration of " ^ description) #>
-  PureThy.add_thms_dynamic (Binding.name name, Data.get);
+  PureThy.add_thms_dynamic (Binding.name name, content);
 
 end;
diff -r c7175a18c090 -r fe551dc9d4bd src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Thu Nov 05 17:59:49 2009 +0100
+++ b/src/Pure/more_thm.ML	Thu Nov 05 20:40:16 2009 +0100
@@ -48,6 +48,7 @@
   val add_thm: thm -> thm list -> thm list
   val del_thm: thm -> thm list -> thm list
   val merge_thms: thm list * thm list -> thm list
+  val full_rules: thm Item_Net.T
   val intro_rules: thm Item_Net.T
   val elim_rules: thm Item_Net.T
   val elim_implies: thm -> thm -> thm
@@ -246,6 +247,7 @@
 val del_thm = remove eq_thm_prop;
 val merge_thms = merge eq_thm_prop;
 
+val full_rules = Item_Net.init eq_thm_prop (single o Thm.full_prop_of);
 val intro_rules = Item_Net.init eq_thm_prop (single o Thm.concl_of);
 val elim_rules = Item_Net.init eq_thm_prop (single o Thm.major_prem_of);