--- a/src/Pure/library.ML Sun Dec 21 22:49:40 2014 +0100
+++ b/src/Pure/library.ML Mon Dec 22 14:33:53 2014 +0100
@@ -199,11 +199,6 @@
val untag_list: (int * 'a) list -> 'a list
val order_list: (int * 'a) list -> 'a list
- (*random numbers*)
- exception RANDOM
- val random: unit -> real
- val random_range: int -> int -> int
-
(*misc*)
val divide_and_conquer: ('a -> 'a list * ('b list -> 'b)) -> 'a -> 'b
val divide_and_conquer': ('a -> 'b -> ('a list * ('c list * 'b -> 'c * 'b)) * 'b) ->
@@ -985,30 +980,6 @@
-(** random numbers **)
-
-exception RANDOM;
-
-fun rmod x y = x - y * Real.realFloor (x / y);
-
-local
- val a = 16807.0;
- val m = 2147483647.0;
- val random_seed = Unsynchronized.ref 1.0;
-in
-
-fun random () = CRITICAL (fn () =>
- let val r = rmod (a * ! random_seed) m
- in (random_seed := r; r) end);
-
-end;
-
-fun random_range l h =
- if h < l orelse l < 0 then raise RANDOM
- else l + Real.floor (rmod (random ()) (real (h - l + 1)));
-
-
-
(** misc **)
fun divide_and_conquer decomp x =