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);

--- 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);