--- a/src/Pure/Tools/named_thms.ML Fri Apr 23 16:12:57 2010 +0200
+++ b/src/Pure/Tools/named_thms.ML Fri Apr 23 18:30:01 2010 +0200
@@ -6,6 +6,7 @@
signature NAMED_THMS =
sig
+ val member: Proof.context -> thm -> bool
val get: Proof.context -> thm list
val add_thm: thm -> Context.generic -> Context.generic
val del_thm: thm -> Context.generic -> Context.generic
@@ -25,6 +26,8 @@
val merge = Item_Net.merge;
);
+val member = Item_Net.member o Data.get o Context.Proof;
+
val content = Item_Net.content o Data.get;
val get = content o Context.Proof;