Datatype_Universe: hide base names only;
authorwenzelm
Tue, 22 Nov 2005 19:37:36 +0100
changeset 18230 4dc1f30af6a1
parent 18229 e5a624483a23
child 18231 2eea98bbf650
Datatype_Universe: hide base names only;
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 *}