# HG changeset patch
# User haftmann
# Date 1186758609 -7200
# Node ID 86f228ce1aef2ed5b2380b6b3e65fb4b0536cd27
# Parent  348e982c694b70ea06f2ad0bbc0bae0a8c24e434
tuned

diff -r 348e982c694b -r 86f228ce1aef src/HOL/ex/Random.thy
--- a/src/HOL/ex/Random.thy	Fri Aug 10 17:10:06 2007 +0200
+++ b/src/HOL/ex/Random.thy	Fri Aug 10 17:10:09 2007 +0200
@@ -171,13 +171,18 @@
 end;
 *}
 
+code_reserved SML Random
+
 code_type randseed
   (SML "Random.seed")
+types_code randseed ("Random.seed")
 
 code_const random_int
   (SML "Random.value")
+consts_code random_int ("Random.value")
 
 code_const run_random
-  (SML "case _ (Random.seed ()) of (x, '_) => x")
+  (SML "case (Random.seed ()) of (x, '_) => _ x")
+consts_code run_random ("case (Random.seed ()) of (x, '_) => _ x")
 
 end