src/HOL/Random.thy

--- a/src/HOL/Random.thy	Mon Mar 29 17:30:36 2010 +0200
+++ b/src/HOL/Random.thy	Mon Mar 29 17:30:38 2010 +0200
@@ -1,3 +1,4 @@
+
 (* Author: Florian Haftmann, TU Muenchen *)
 
 header {* A HOL random engine *}
@@ -154,6 +155,14 @@
 
 in
 
+fun next_seed () =
+  let
+    val (seed1, seed') = @{code split_seed} (! seed)
+    val _ = seed := seed'
+  in
+    seed1
+  end
+
 fun run f =
   let
     val (x, seed') = f (! seed);