separate module Random;
proper Synchronized.var;

--- a/src/HOL/Matrix_LP/Compute_Oracle/am_sml.ML	Sun Dec 21 22:49:40 2014 +0100
+++ b/src/HOL/Matrix_LP/Compute_Oracle/am_sml.ML	Mon Dec 22 14:33:53 2014 +0100
@@ -12,7 +12,7 @@
   val save_result : (string * term) -> unit
   val set_compiled_rewriter : (term -> term) -> unit
   val list_nth : 'a list * int -> 'a
-  val dump_output : (string option) Unsynchronized.ref 
+  val dump_output : string option Unsynchronized.ref 
 end
 
 structure AM_SML : AM_SML = struct
@@ -490,7 +490,7 @@
 fun compile rules = 
     let
         val guid = get_guid ()
-        val code = Real.toString (random ())
+        val code = Real.toString (Random.random ())
         val name = "AMSML_"^guid
         val (inlinetab, source) = sml_prog name code rules
         val _ = case !dump_output of NONE => () | SOME p => writeTextFile p source

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Sun Dec 21 22:49:40 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Mon Dec 22 14:33:53 2014 +0100
@@ -1434,7 +1434,7 @@
               val max_isar = 1000 * max_dependencies
 
               fun priority_of th =
-                random_range 0 max_isar +
+                Random.random_range 0 max_isar +
                 (case try (Graph.get_node access_G) (nickname_of_thm th) of
                   SOME (Isar_Proof, _, deps) => ~100 * length deps
                 | SOME (Automatic_Proof, _, _) => 2 * max_isar

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Sun Dec 21 22:49:40 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Mon Dec 22 14:33:53 2014 +0100
@@ -351,10 +351,9 @@
       with_cleanup clean_up run () |> tap export
 
     val important_message =
-      if mode = Normal andalso random_range 0 (atp_important_message_keep_quotient - 1) = 0 then
-        extract_important_message output
-      else
-        ""
+      if mode = Normal andalso Random.random_range 0 (atp_important_message_keep_quotient - 1) = 0
+      then extract_important_message output
+      else ""
 
     val (used_facts, preferred_methss, message) =
       (case outcome of

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Concurrent/random.ML	Mon Dec 22 14:33:53 2014 +0100
@@ -0,0 +1,38 @@
+(*  Title:      Pure/Confurrent/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;
+

--- a/src/Pure/ROOT	Sun Dec 21 22:49:40 2014 +0100
+++ b/src/Pure/ROOT	Mon Dec 22 14:33:53 2014 +0100
@@ -62,6 +62,7 @@
     "Concurrent/par_exn.ML"
     "Concurrent/par_list.ML"
     "Concurrent/par_list_sequential.ML"
+    "Concurrent/random.ML"
     "Concurrent/simple_thread.ML"
     "Concurrent/single_assignment.ML"
     "Concurrent/single_assignment_sequential.ML"

--- a/src/Pure/ROOT.ML	Sun Dec 21 22:49:40 2014 +0100
+++ b/src/Pure/ROOT.ML	Mon Dec 22 14:33:53 2014 +0100
@@ -22,6 +22,7 @@
 if Multithreading.available then ()
 else use "Concurrent/synchronized_sequential.ML";
 use "Concurrent/counter.ML";
+use "Concurrent/random.ML";
 
 use "General/properties.ML";
 use "General/output.ML";

--- 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 =