# HG changeset patch
# User wenzelm
# Date 1288297391 -7200
# Node ID edcdecd556556668acdce206c363ab05762fbeb7
# Parent  96fff8c0a85364b6f2da22f40f284b306317f9ca
type attribute is derived concept outside the kernel;

diff -r 96fff8c0a853 -r edcdecd55655 src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Thu Oct 28 22:12:08 2010 +0200
+++ b/src/Pure/more_thm.ML	Thu Oct 28 22:23:11 2010 +0200
@@ -12,6 +12,7 @@
   structure Ctermtab: TABLE
   structure Thmtab: TABLE
   val aconvc: cterm * cterm -> bool
+  type attribute = Context.generic * thm -> Context.generic * thm
 end;
 
 signature THM =
@@ -64,6 +65,7 @@
   val close_derivation: thm -> thm
   val add_axiom: binding * term -> theory -> (string * thm) * theory
   val add_def: bool -> bool -> binding * term -> theory -> (string * thm) * theory
+  type attribute = Context.generic * thm -> Context.generic * thm
   type binding = binding * attribute list
   val empty_binding: binding
   val rule_attribute: (Context.generic -> thm -> thm) -> attribute
@@ -382,6 +384,9 @@
 
 (** attributes **)
 
+(*attributes subsume any kind of rules or context modifiers*)
+type attribute = Context.generic * thm -> Context.generic * thm;
+
 type binding = binding * attribute list;
 val empty_binding: binding = (Binding.empty, []);
 
diff -r 96fff8c0a853 -r edcdecd55655 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Thu Oct 28 22:12:08 2010 +0200
+++ b/src/Pure/thm.ML	Thu Oct 28 22:23:11 2010 +0200
@@ -39,7 +39,6 @@
   (*theorems*)
   type thm
   type conv = cterm -> thm
-  type attribute = Context.generic * thm -> Context.generic * thm
   val rep_thm: thm ->
    {thy_ref: theory_ref,
     tags: Properties.T,
@@ -350,9 +349,6 @@
 
 type conv = cterm -> thm;
 
-(*attributes subsume any kind of rules or context modifiers*)
-type attribute = Context.generic * thm -> Context.generic * thm;
-
 (*errors involving theorems*)
 exception THM of string * int * thm list;