src/Pure/Tools/named_thms.ML
changeset 36296 5cc547abd995
parent 33519 e31a85f92ce9
child 39557 fe5722fce758
     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