# HG changeset patch
# User wenzelm
# Date 1137880945 -3600
# Node ID 0508c80178395e81810a93c57e054da476f9037d
# Parent  c0511e120f176c2ac6b9ecff25d4ce02f4999ef5
simplified type attribute;
added rule/declaration_attribute (from drule.ML);
added theory/proof_attributes;
removed apply(s)_attributes;

diff -r c0511e120f17 -r 0508c8017839 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Sat Jan 21 23:02:24 2006 +0100
+++ b/src/Pure/thm.ML	Sat Jan 21 23:02:25 2006 +0100
@@ -71,7 +71,7 @@
     tpairs: (cterm * cterm) list,
     prop: cterm}
   exception THM of string * int * thm list
-  type 'a attribute     (* = 'a * thm -> 'a * thm *)
+  type attribute     (* = Context.generic * thm -> Context.generic * thm *)
   val eq_thm: thm * thm -> bool
   val eq_thms: thm list * thm list -> bool
   val theory_of_thm: thm -> theory
@@ -141,10 +141,12 @@
   val cabs: cterm -> cterm -> cterm
   val major_prem_of: thm -> term
   val no_prems: thm -> bool
+  val rule_attribute: (Context.generic -> thm -> thm) -> attribute
+  val declaration_attribute: (thm -> Context.generic -> Context.generic) -> attribute
+  val theory_attributes: attribute list -> theory * thm -> theory * thm
+  val proof_attributes: attribute list -> Context.proof * thm -> Context.proof * thm
   val no_attributes: 'a -> 'a * 'b list
   val simple_fact: 'a -> ('a * 'b list) list
-  val apply_attributes: 'a attribute list -> 'a * thm -> 'a * thm
-  val applys_attributes: 'a attribute list -> 'a * thm list -> 'a * thm list
   val terms_of_tpairs: (term * term) list -> term list
   val full_prop_of: thm -> term
   val get_name_tags: thm -> string * tag list
@@ -397,12 +399,22 @@
 
 
 (*attributes subsume any kind of rules or context modifiers*)
-type 'a attribute = 'a * thm -> 'a * thm;
+type attribute = Context.generic * thm -> Context.generic * thm;
+
+fun rule_attribute f (x, th) = (x, f x th);
+fun declaration_attribute f (x, th) = (f th x, th);
+
+fun apply_attributes mk dest =
+  let
+    fun app [] = I
+      | app ((f: attribute) :: fs) = fn (x, th) => f (mk x, th) |>> dest |> app fs;
+  in app end;
+
+val theory_attributes = apply_attributes Context.Theory Context.the_theory;
+val proof_attributes = apply_attributes Context.Proof Context.the_proof;
 
 fun no_attributes x = (x, []);
 fun simple_fact x = [(x, [])];
-val apply_attributes = Library.apply;
-fun applys_attributes atts = foldl_map (Library.apply atts);
 
 
 (* hyps *)