--- a/src/Pure/more_thm.ML Tue Mar 03 13:22:01 2009 +0100
+++ b/src/Pure/more_thm.ML Tue Mar 03 14:07:23 2009 +0100
@@ -40,6 +40,8 @@
val close_derivation: thm -> thm
val add_axiom: binding * term -> theory -> thm * theory
val add_def: bool -> bool -> binding * term -> theory -> thm * theory
+ type binding = binding * attribute list
+ val empty_binding: binding
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
@@ -301,6 +303,9 @@
(** attributes **)
+type binding = binding * attribute list;
+val empty_binding: binding = (Binding.empty, []);
+
fun rule_attribute f (x, th) = (x, f x th);
fun declaration_attribute f (x, th) = (f th x, th);