src/Pure/more_thm.ML
changeset 45382 3a9f84ad31e7
parent 45375 7fe19930dfc9
child 46497 89ccf66aa73d
--- a/src/Pure/more_thm.ML	Sun Nov 06 22:18:54 2011 +0100
+++ b/src/Pure/more_thm.ML	Mon Nov 07 12:08:22 2011 +0100
@@ -403,7 +403,7 @@
 fun declaration_attribute f (x, th) = (SOME (f th x), NONE);
 fun mixed_attribute f (x, th) = let val (x', th') = f (x, th) in (SOME x', SOME th') end;
 
-fun apply_attribute att (x, th) =
+fun apply_attribute (att: attribute) (x, th) =
   let val (x', th') = att (x, th)
   in (the_default x x', the_default th th') end;