export add/del_thm;
authorwenzelm
Thu Mar 20 16:04:34 2008 +0100 (2008-03-20 ago)
changeset 263639d95309f8069
parent 26362 d9ce159a41d1
child 26364 cb6f360ab425
export add/del_thm;
src/Pure/Tools/named_thms.ML
     1.1 --- a/src/Pure/Tools/named_thms.ML	Thu Mar 20 16:04:32 2008 +0100
     1.2 +++ b/src/Pure/Tools/named_thms.ML	Thu Mar 20 16:04:34 2008 +0100
     1.3 @@ -9,6 +9,8 @@
     1.4  sig
     1.5    val get: Proof.context -> thm list
     1.6    val pretty: Proof.context -> Pretty.T
     1.7 +  val add_thm: thm -> Context.generic -> Context.generic
     1.8 +  val del_thm: thm -> Context.generic -> Context.generic
     1.9    val add: attribute
    1.10    val del: attribute
    1.11    val setup: theory -> theory
    1.12 @@ -30,8 +32,11 @@
    1.13  fun pretty ctxt =
    1.14    Pretty.big_list (description ^ ":") (map (ProofContext.pretty_thm ctxt) (get ctxt));
    1.15  
    1.16 -val add = Thm.declaration_attribute (Data.map o Thm.add_thm);
    1.17 -val del = Thm.declaration_attribute (Data.map o Thm.del_thm);
    1.18 +val add_thm = Data.map o Thm.add_thm;
    1.19 +val del_thm = Data.map o Thm.del_thm;
    1.20 +
    1.21 +val add = Thm.declaration_attribute add_thm;
    1.22 +val del = Thm.declaration_attribute del_thm;
    1.23  
    1.24  val setup =
    1.25    Attrib.add_attributes [(name, Attrib.add_del_args add del, "declaration of " ^ description)];