tuned
authorhaftmann
Fri Aug 10 17:10:09 2007 +0200 (2007-08-10)
changeset 2422686f228ce1aef
parent 24225 348e982c694b
child 24227 9b226b56e9a9
tuned
src/HOL/ex/Random.thy
     1.1 --- a/src/HOL/ex/Random.thy	Fri Aug 10 17:10:06 2007 +0200
     1.2 +++ b/src/HOL/ex/Random.thy	Fri Aug 10 17:10:09 2007 +0200
     1.3 @@ -171,13 +171,18 @@
     1.4  end;
     1.5  *}
     1.6  
     1.7 +code_reserved SML Random
     1.8 +
     1.9  code_type randseed
    1.10    (SML "Random.seed")
    1.11 +types_code randseed ("Random.seed")
    1.12  
    1.13  code_const random_int
    1.14    (SML "Random.value")
    1.15 +consts_code random_int ("Random.value")
    1.16  
    1.17  code_const run_random
    1.18 -  (SML "case _ (Random.seed ()) of (x, '_) => x")
    1.19 +  (SML "case (Random.seed ()) of (x, '_) => _ x")
    1.20 +consts_code run_random ("case (Random.seed ()) of (x, '_) => _ x")
    1.21  
    1.22  end