src/HOL/Datatype.thy
changeset 14274 0cb8a9a144d2
parent 14208 144f45277d5a
child 14981 e73f8140af78
     1.1 --- a/src/HOL/Datatype.thy	Thu Dec 04 16:16:36 2003 +0100
     1.2 +++ b/src/HOL/Datatype.thy	Thu Dec 04 21:57:15 2003 +0100
     1.3 @@ -78,7 +78,7 @@
     1.4  subsection {* Finishing the datatype package setup *}
     1.5  
     1.6  text {* Belongs to theory @{text Datatype_Universe}; hides popular names. *}
     1.7 -hide const Node Atom Leaf Numb Lim Split Case Suml Sumr
     1.8 +hide const Push Node Atom Leaf Numb Lim Split Case Suml Sumr
     1.9  hide type node item
    1.10  
    1.11