# HG changeset patch
# User wenzelm
# Date 1377525429 -7200
# Node ID 5d2fe75c6306e2af720a1cf80e535959ee8bd620
# Parent  8d41170242cb23b578d77a8719016226dd7393ee
always transfer thm where attributes are applied -- relevant for internal 'notes' (e.g. via bundle 'includes') in contrast to external 'notes' (cf. Proof_Context.retrieve_thms);

diff -r 8d41170242cb -r 5d2fe75c6306 src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Mon Aug 26 15:45:51 2013 +0200
+++ b/src/Pure/more_thm.ML	Mon Aug 26 15:57:09 2013 +0200
@@ -407,7 +407,7 @@
 fun mixed_attribute f (x, th) = let val (x', th') = f (x, th) in (SOME x', SOME th') end;
 
 fun apply_attribute (att: attribute) th x =
-  let val (x', th') = att (x, th)
+  let val (x', th') = att (x, Thm.transfer (Context.theory_of x) th)
   in (the_default th th', the_default x x') end;
 
 fun attribute_declaration att th x = #2 (apply_attribute att th x);