# HG changeset patch
# User wenzelm
# Date 1132684656 -3600
# Node ID 4dc1f30af6a1ccedb21087eabb886beadcbb5d95
# Parent  e5a624483a23c1a3ba85fad153a22f07fff15673
Datatype_Universe: hide base names only;

diff -r e5a624483a23 -r 4dc1f30af6a1 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 *}