1.1 --- a/src/HOL/Random.thy	Mon Mar 29 17:30:36 2010 +0200
     1.2 +++ b/src/HOL/Random.thy	Mon Mar 29 17:30:38 2010 +0200
     1.3 @@ -1,3 +1,4 @@
     1.4 +
     1.5  (* Author: Florian Haftmann, TU Muenchen *)
     1.6  
     1.7  header {* A HOL random engine *}
     1.8 @@ -154,6 +155,14 @@
     1.9  
    1.10  in
    1.11  
    1.12 +fun next_seed () =
    1.13 +  let
    1.14 +    val (seed1, seed') = @{code split_seed} (! seed)
    1.15 +    val _ = seed := seed'
    1.16 +  in
    1.17 +    seed1
    1.18 +  end
    1.19 +
    1.20  fun run f =
    1.21    let
    1.22      val (x, seed') = f (! seed);