# HG changeset patch
# User wenzelm
# Date 1358365250 -3600
# Node ID 697e3bb60a3bc45d97c907b348c33a77ed31150c
# Parent  8d391f185caccfc606dee811f2bd8a95e5ca0796
eliminated dead code;

diff -r 8d391f185cac -r 697e3bb60a3b src/Pure/library.ML
--- a/src/Pure/library.ML	Wed Jan 16 18:43:59 2013 +0100
+++ b/src/Pure/library.ML	Wed Jan 16 20:40:50 2013 +0100
@@ -204,8 +204,6 @@
   exception RANDOM
   val random: unit -> real
   val random_range: int -> int -> int
-  val one_of: 'a list -> 'a
-  val frequency: (int * 'a) list -> 'a
 
   (*misc*)
   val divide_and_conquer: ('a -> 'a list * ('b list -> 'b)) -> 'a -> 'b
@@ -1021,15 +1019,6 @@
   if h < l orelse l < 0 then raise RANDOM
   else l + Real.floor (rmod (random ()) (real (h - l + 1)));
 
-fun one_of xs = nth xs (random_range 0 (length xs - 1));
-
-fun frequency xs =
-  let
-    val sum = foldl op + (0, map fst 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;
-
 
 
 (** misc **)