author | wenzelm |
Mon, 07 Nov 2011 12:08:22 +0100 | |
changeset 45382 | 3a9f84ad31e7 |
parent 45381 | d17e7b4422e8 |
child 45383 | bf6add30ab20 |
child 45386 | cfc8a0661310 |
--- 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;