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