# HG changeset patch
# User haftmann
# Date 1272547336 -7200
# Node ID 4fe16d49283bfbf3dc986a0ad6e9e7f12c397a6d
# Parent  b0186c66f3240f10ab2d7a48107daf9ae39db947
make random engine persistent using code_reflect

diff -r b0186c66f324 -r 4fe16d49283b src/HOL/Random.thy
--- a/src/HOL/Random.thy	Thu Apr 29 15:00:43 2010 +0200
+++ b/src/HOL/Random.thy	Thu Apr 29 15:22:16 2010 +0200
@@ -138,10 +138,15 @@
 
 subsection {* @{text ML} interface *}
 
+code_reflect Random_Engine
+  functions range select select_weight
+
 ML {*
 structure Random_Engine =
 struct
 
+open Random_Engine;
+
 type seed = int * int;
 
 local