--- 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)];