summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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