check_hyps when attributes are applied;

--- a/src/Pure/more_thm.ML	Sat Jan 11 23:35:05 2014 +0100
+++ b/src/Pure/more_thm.ML	Sat Jan 11 23:53:38 2014 +0100
@@ -453,7 +453,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, (* check_hyps x *) (* FIXME *) (Thm.transfer (Context.theory_of x) th))
+  let val (x', th') = att (x, check_hyps 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);