src/Pure/library.ML
changeset 17756 d4a35f82fbb4
parent 17545 1ba448f96af1
child 17819 1241e5d31d5b
     1.1 --- a/src/Pure/library.ML	Tue Oct 04 16:47:40 2005 +0200
     1.2 +++ b/src/Pure/library.ML	Tue Oct 04 19:01:37 2005 +0200
     1.3 @@ -1165,7 +1165,7 @@
     1.4  fun frequency xs =
     1.5    let
     1.6      val sum = foldl op + (0, map fst xs);
     1.7 -    fun pick n ((k, x) :: xs) =
     1.8 +    fun pick n ((k: int, x) :: xs) =
     1.9        if n <= k then x else pick (n - k) xs
    1.10    in pick (random_range 1 sum) xs end;
    1.11