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