src/HOL/Datatype.thy
changeset 36176 3fe7e97ccca8
parent 35216 7641e8d831d2
child 39198 f967a16dfcdd
     1.1 --- a/src/HOL/Datatype.thy	Fri Apr 16 20:56:40 2010 +0200
     1.2 +++ b/src/HOL/Datatype.thy	Fri Apr 16 21:28:09 2010 +0200
     1.3 @@ -512,8 +512,8 @@
     1.4  
     1.5  
     1.6  text {* hides popular names *}
     1.7 -hide (open) type node item
     1.8 -hide (open) const Push Node Atom Leaf Numb Lim Split Case
     1.9 +hide_type (open) node item
    1.10 +hide_const (open) Push Node Atom Leaf Numb Lim Split Case
    1.11  
    1.12  use "Tools/Datatype/datatype.ML"
    1.13