src/HOL/Datatype.thy

--- a/src/HOL/Datatype.thy	Tue Nov 22 19:34:50 2005 +0100
+++ b/src/HOL/Datatype.thy	Tue Nov 22 19:37:36 2005 +0100
@@ -79,8 +79,8 @@
 subsection {* Finishing the datatype package setup *}
 
 text {* Belongs to theory @{text Datatype_Universe}; hides popular names. *}
-hide const Push Node Atom Leaf Numb Lim Split Case Suml Sumr
-hide type node item
+hide (open) const Push Node Atom Leaf Numb Lim Split Case Suml Sumr
+hide (open) type node item
 
 
 subsection {* Further cases/induct rules for tuples *}