diff -r b0cd55afead1 -r d4a35f82fbb4 src/Pure/library.ML
--- a/src/Pure/library.ML	Tue Oct 04 16:47:40 2005 +0200
+++ b/src/Pure/library.ML	Tue Oct 04 19:01:37 2005 +0200
@@ -1165,7 +1165,7 @@
 fun frequency xs =
   let
     val sum = foldl op + (0, map fst xs);
-    fun pick n ((k, x) :: xs) =
+    fun pick n ((k: int, x) :: xs) =
       if n <= k then x else pick (n - k) xs
   in pick (random_range 1 sum) xs end;