# HG changeset patch
# User wenzelm
# Date 1457600189 -3600
# Node ID 5d4ed917450d180f53f96ba26e4ccb73e3b4f7fd
# Parent  6cd36a0d2a289fe5ce9d1c914443a16627580aab
clarified files;

diff -r 6cd36a0d2a28 -r 5d4ed917450d src/Pure/Concurrent/random.ML
--- a/src/Pure/Concurrent/random.ML	Thu Mar 10 09:50:53 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,38 +0,0 @@
-(*  Title:      Pure/Concurrent/random.ML
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-
-Pseudo random numbers.
-*)
-
-signature RANDOM =
-sig
-  val random: unit -> real
-  exception RANDOM
-  val random_range: int -> int -> int
-end;
-
-structure Random: RANDOM =
-struct
-
-fun rmod x y = x - y * Real.realFloor (x / y);
-
-local
-  val a = 16807.0;
-  val m = 2147483647.0;
-  val random_seed = Synchronized.var "random_seed" 1.0;
-in
-
-fun random () =
-  Synchronized.change_result random_seed
-    (fn r => let val r' = rmod (a * r) m in (r', r') end);
-
-end;
-
-exception RANDOM;
-
-fun random_range l h =
-  if h < l orelse l < 0 then raise RANDOM
-  else l + Real.floor (rmod (random ()) (real (h - l + 1)));
-
-end;
-
diff -r 6cd36a0d2a28 -r 5d4ed917450d src/Pure/General/random.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/random.ML	Thu Mar 10 09:56:29 2016 +0100
@@ -0,0 +1,38 @@
+(*  Title:      Pure/General/random.ML
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
+
+Pseudo random numbers.
+*)
+
+signature RANDOM =
+sig
+  val random: unit -> real
+  exception RANDOM
+  val random_range: int -> int -> int
+end;
+
+structure Random: RANDOM =
+struct
+
+fun rmod x y = x - y * Real.realFloor (x / y);
+
+local
+  val a = 16807.0;
+  val m = 2147483647.0;
+  val random_seed = Synchronized.var "random_seed" 1.0;
+in
+
+fun random () =
+  Synchronized.change_result random_seed
+    (fn r => let val r' = rmod (a * r) m in (r', r') end);
+
+end;
+
+exception RANDOM;
+
+fun random_range l h =
+  if h < l orelse l < 0 then raise RANDOM
+  else l + Real.floor (rmod (random ()) (real (h - l + 1)));
+
+end;
+
diff -r 6cd36a0d2a28 -r 5d4ed917450d src/Pure/ROOT
--- a/src/Pure/ROOT	Thu Mar 10 09:50:53 2016 +0100
+++ b/src/Pure/ROOT	Thu Mar 10 09:56:29 2016 +0100
@@ -12,7 +12,6 @@
     "Concurrent/multithreading.ML"
     "Concurrent/par_exn.ML"
     "Concurrent/par_list.ML"
-    "Concurrent/random.ML"
     "Concurrent/single_assignment.ML"
     "Concurrent/standard_thread.ML"
     "Concurrent/synchronized.ML"
@@ -45,6 +44,7 @@
     "General/print_mode.ML"
     "General/properties.ML"
     "General/queue.ML"
+    "General/random.ML"
     "General/same.ML"
     "General/scan.ML"
     "General/secure.ML"
diff -r 6cd36a0d2a28 -r 5d4ed917450d src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Thu Mar 10 09:50:53 2016 +0100
+++ b/src/Pure/ROOT.ML	Thu Mar 10 09:56:29 2016 +0100
@@ -107,8 +107,8 @@
 
 use "Concurrent/synchronized.ML";
 use "Concurrent/counter.ML";
-use "Concurrent/random.ML";
 
+use "General/random.ML";
 use "General/properties.ML";
 use "General/output.ML";
 use "PIDE/markup.ML";