# HG changeset patch
# User wenzelm
# Date 1320664102 -3600
# Node ID 3a9f84ad31e7115ba1ebde0a4171f6d46d7c0bbf
# Parent  d17e7b4422e861efa91f17cb89fd873399631588
made SML/NJ happy;

diff -r d17e7b4422e8 -r 3a9f84ad31e7 src/Pure/more_thm.ML
--- 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;