Item_Net/Named_Thms: export efficient member operation;
authorwenzelm
Fri Apr 23 18:30:01 2010 +0200 (2010-04-23 ago)
changeset 362965cc547abd995
parent 36295 9eaaa05c972c
child 36297 6b2b9516a3cd
Item_Net/Named_Thms: export efficient member operation;
src/Pure/Tools/named_thms.ML
src/Pure/item_net.ML
     1.1 --- a/src/Pure/Tools/named_thms.ML	Fri Apr 23 16:12:57 2010 +0200
     1.2 +++ b/src/Pure/Tools/named_thms.ML	Fri Apr 23 18:30:01 2010 +0200
     1.3 @@ -6,6 +6,7 @@
     1.4  
     1.5  signature NAMED_THMS =
     1.6  sig
     1.7 +  val member: Proof.context -> thm -> bool
     1.8    val get: Proof.context -> thm list
     1.9    val add_thm: thm -> Context.generic -> Context.generic
    1.10    val del_thm: thm -> Context.generic -> Context.generic
    1.11 @@ -25,6 +26,8 @@
    1.12    val merge = Item_Net.merge;
    1.13  );
    1.14  
    1.15 +val member = Item_Net.member o Data.get o Context.Proof;
    1.16 +
    1.17  val content = Item_Net.content o Data.get;
    1.18  val get = content o Context.Proof;
    1.19  
     2.1 --- a/src/Pure/item_net.ML	Fri Apr 23 16:12:57 2010 +0200
     2.2 +++ b/src/Pure/item_net.ML	Fri Apr 23 18:30:01 2010 +0200
     2.3 @@ -11,6 +11,7 @@
     2.4    val init: ('a * 'a -> bool) -> ('a -> term list) -> 'a T
     2.5    val content: 'a T -> 'a list
     2.6    val retrieve: 'a T -> term -> 'a list
     2.7 +  val member: 'a T -> 'a -> bool
     2.8    val merge: 'a T * 'a T -> 'a T
     2.9    val remove: 'a -> 'a T -> 'a T
    2.10    val update: 'a -> 'a T -> 'a T
    2.11 @@ -49,7 +50,6 @@
    2.12    mk_items eq index (x :: content) (next - 1)
    2.13      (fold (fn t => Net.insert_term (K false) (t, (next, x))) (index x) net);
    2.14  
    2.15 -
    2.16  fun merge (items1, Items {content = content2, ...}) =
    2.17    fold_rev (fn y => if member items1 y then I else cons y) content2 items1;
    2.18