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