# HG changeset patch
# User wenzelm
# Date 1389480818 -3600
# Node ID aee15e11ee732084af288d038374dd03a63224fd
# Parent  68228c162ed547dbeb209d0583ec6758a6a60e0e
check_hyps when attributes are applied;

diff -r 68228c162ed5 -r aee15e11ee73 src/Pure/more_thm.ML
--- 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);