diff -r 5cec4ca719d1 -r 3fe7e97ccca8 src/HOL/Random.thy
--- a/src/HOL/Random.thy	Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/Random.thy	Fri Apr 16 21:28:09 2010 +0200
@@ -174,10 +174,10 @@
 end;
 *}
 
-hide (open) type seed
-hide (open) const inc_shift minus_shift log "next" split_seed
+hide_type (open) seed
+hide_const (open) inc_shift minus_shift log "next" split_seed
   iterate range select pick select_weight
-hide (open) fact range_def
+hide_fact (open) range_def
 
 no_notation fcomp (infixl "o>" 60)
 no_notation scomp (infixl "o\<rightarrow>" 60)