1.1 --- a/src/Pure/more_thm.ML	Thu Oct 28 22:12:08 2010 +0200
     1.2 +++ b/src/Pure/more_thm.ML	Thu Oct 28 22:23:11 2010 +0200
     1.3 @@ -12,6 +12,7 @@
     1.4    structure Ctermtab: TABLE
     1.5    structure Thmtab: TABLE
     1.6    val aconvc: cterm * cterm -> bool
     1.7 +  type attribute = Context.generic * thm -> Context.generic * thm
     1.8  end;
     1.9  
    1.10  signature THM =
    1.11 @@ -64,6 +65,7 @@
    1.12    val close_derivation: thm -> thm
    1.13    val add_axiom: binding * term -> theory -> (string * thm) * theory
    1.14    val add_def: bool -> bool -> binding * term -> theory -> (string * thm) * theory
    1.15 +  type attribute = Context.generic * thm -> Context.generic * thm
    1.16    type binding = binding * attribute list
    1.17    val empty_binding: binding
    1.18    val rule_attribute: (Context.generic -> thm -> thm) -> attribute
    1.19 @@ -382,6 +384,9 @@
    1.20  
    1.21  (** attributes **)
    1.22  
    1.23 +(*attributes subsume any kind of rules or context modifiers*)
    1.24 +type attribute = Context.generic * thm -> Context.generic * thm;
    1.25 +
    1.26  type binding = binding * attribute list;
    1.27  val empty_binding: binding = (Binding.empty, []);
    1.28  

     2.1 --- a/src/Pure/thm.ML	Thu Oct 28 22:12:08 2010 +0200
     2.2 +++ b/src/Pure/thm.ML	Thu Oct 28 22:23:11 2010 +0200
     2.3 @@ -39,7 +39,6 @@
     2.4    (*theorems*)
     2.5    type thm
     2.6    type conv = cterm -> thm
     2.7 -  type attribute = Context.generic * thm -> Context.generic * thm
     2.8    val rep_thm: thm ->
     2.9     {thy_ref: theory_ref,
    2.10      tags: Properties.T,
    2.11 @@ -350,9 +349,6 @@
    2.12  
    2.13  type conv = cterm -> thm;
    2.14  
    2.15 -(*attributes subsume any kind of rules or context modifiers*)
    2.16 -type attribute = Context.generic * thm -> Context.generic * thm;
    2.17 -
    2.18  (*errors involving theorems*)
    2.19  exception THM of string * int * thm list;
    2.20