diff -r 5cec4ca719d1 -r 3fe7e97ccca8 src/HOL/Predicate.thy
--- a/src/HOL/Predicate.thy	Fri Apr 16 20:56:40 2010 +0200
+++ b/src/HOL/Predicate.thy	Fri Apr 16 21:28:09 2010 +0200
@@ -934,8 +934,8 @@
   bot ("\<bottom>") and
   bind (infixl "\<guillemotright>=" 70)
 
-hide (open) type pred seq
-hide (open) const Pred eval single bind is_empty singleton if_pred not_pred holds
+hide_type (open) pred seq
+hide_const (open) Pred eval single bind is_empty singleton if_pred not_pred holds
   Empty Insert Join Seq member pred_of_seq "apply" adjunct null the_only eq map not_unique the
 
 end