| changeset 17756 | d4a35f82fbb4 |
| parent 17545 | 1ba448f96af1 |
| child 17819 | 1241e5d31d5b |
--- 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;