# HG changeset patch
# User wenzelm
# Date 1136918012 -3600
# Node ID b32ee57b35f7c03449857afd5a588ef9080ecd43
# Parent  3149c6abe8760e0f3863c803e2f542e59665c14e
added declaration_attribute;

diff -r 3149c6abe876 -r b32ee57b35f7 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Tue Jan 10 19:33:31 2006 +0100
+++ b/src/Pure/drule.ML	Tue Jan 10 19:33:32 2006 +0100
@@ -93,6 +93,7 @@
   val plain_prop_of: thm -> term
   val add_used: thm -> string list -> string list
   val rule_attribute: ('a -> thm -> thm) -> 'a attribute
+  val declaration_attribute: (thm -> 'a -> 'a) -> 'a attribute
   val map_tags: (tag list -> tag list) -> thm -> thm
   val tag_rule: tag -> thm -> thm
   val untag_rule: string -> thm -> thm
@@ -325,9 +326,8 @@
 
 (** basic attributes **)
 
-(* dependent rules *)
-
-fun rule_attribute f (x, thm) = (x, (f x thm));
+fun rule_attribute f (x, th) = (x, f x th);
+fun declaration_attribute f (x, th) = (f th x, th);
 
 
 (* add / delete tags *)