diff -r 9e245d524997 -r 225fa48756b2 src/Pure/more_thm.ML
--- 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);