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;