# HG changeset patch
# User wenzelm
# Date 1206025474 -3600
# Node ID 9d95309f806954ca166c0ccdcc5cd6ae1693bec4
# Parent  d9ce159a41d1ace59e8cb0b3bf711030fb8d1ea6
export add/del_thm;

diff -r d9ce159a41d1 -r 9d95309f8069 src/Pure/Tools/named_thms.ML
--- a/src/Pure/Tools/named_thms.ML	Thu Mar 20 16:04:32 2008 +0100
+++ b/src/Pure/Tools/named_thms.ML	Thu Mar 20 16:04:34 2008 +0100
@@ -9,6 +9,8 @@
 sig
   val get: Proof.context -> thm list
   val pretty: Proof.context -> Pretty.T
+  val add_thm: thm -> Context.generic -> Context.generic
+  val del_thm: thm -> Context.generic -> Context.generic
   val add: attribute
   val del: attribute
   val setup: theory -> theory
@@ -30,8 +32,11 @@
 fun pretty ctxt =
   Pretty.big_list (description ^ ":") (map (ProofContext.pretty_thm ctxt) (get ctxt));
 
-val add = Thm.declaration_attribute (Data.map o Thm.add_thm);
-val del = Thm.declaration_attribute (Data.map o Thm.del_thm);
+val add_thm = Data.map o Thm.add_thm;
+val del_thm = Data.map o Thm.del_thm;
+
+val add = Thm.declaration_attribute add_thm;
+val del = Thm.declaration_attribute del_thm;
 
 val setup =
   Attrib.add_attributes [(name, Attrib.add_del_args add del, "declaration of " ^ description)];