diff -r 5cec4ca719d1 -r 3fe7e97ccca8 src/HOL/New_Random_Sequence.thy
--- a/src/HOL/New_Random_Sequence.thy	Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/New_Random_Sequence.thy	Fri Apr 16 21:28:09 2010 +0200
@@ -91,16 +91,16 @@
 where
   "neg_map f P = neg_bind P (neg_single o f)"
 (*
-hide const DSequence.empty DSequence.single DSequence.eval
+hide_const DSequence.empty DSequence.single DSequence.eval
   DSequence.map_seq DSequence.bind DSequence.union DSequence.if_seq DSequence.not_seq
   DSequence.map
 *)
 
-hide (open) const
+hide_const (open)
   pos_empty pos_single pos_bind pos_union pos_if_random_dseq pos_iterate_upto pos_not_random_dseq iter Random pos_map
   neg_empty neg_single neg_bind neg_union neg_if_random_dseq neg_iterate_upto neg_not_random_dseq neg_map
-hide type New_DSequence.pos_dseq New_DSequence.neg_dseq pos_random_dseq neg_random_dseq
+hide_type New_DSequence.pos_dseq New_DSequence.neg_dseq pos_random_dseq neg_random_dseq
 (* FIXME: hide facts *)
-(*hide (open) fact empty_def single_def bind_def union_def if_random_dseq_def not_random_dseq_def Random.simps map_def*)
+(*hide_fact (open) empty_def single_def bind_def union_def if_random_dseq_def not_random_dseq_def Random.simps map_def*)
 
 end
\ No newline at end of file