diff -r d593d18a7a92 -r fe8d0f4da0e6 src/Tools/Spec_Check/random.ML
--- a/src/Tools/Spec_Check/random.ML	Thu Jul 08 15:25:58 2021 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,46 +0,0 @@
-(*  Title:      Tools/Spec_Check/random.ML
-    Author:     Lukas Bulwahn and Nicolai Schaffroth, TU Muenchen
-    Author:     Christopher League
-
-Random number engine.
-*)
-
-signature RANDOM =
-sig
-  type rand
-  val new : unit -> rand
-  val range : int * int -> rand -> int * rand
-  val split : rand -> rand * rand
-end
-
-structure Random : RANDOM  =
-struct
-
-type rand = real
-
-val a = 16807.0
-val m = 2147483647.0
-
-fun nextrand seed =
-  let
-    val t = a * seed
-  in
-    t - m * real(floor(t/m))
-  end
-
-val new = nextrand o Time.toReal o Time.now
-
-fun range (min, max) =
-  if min > max then raise Domain (* TODO: raise its own error *)
-  else fn r => (min + (floor(real(max-min+1) * r / m)), nextrand r)
-
-fun split r =
-  let
-    val r = r / a
-    val r0 = real(floor r)
-    val r1 = r - r0
-  in
-    (nextrand r0, nextrand r1)
-  end
-
-end