# HG changeset patch
# User nipkow
# Date 1070571435 -3600
# Node ID 0cb8a9a144d2281d9c328b5f59cb6d4d017f99d0
# Parent  e33ffff0123c63559d0fb50ab615d63e49b32be7
hide Push

diff -r e33ffff0123c -r 0cb8a9a144d2 src/HOL/Datatype.thy
--- a/src/HOL/Datatype.thy	Thu Dec 04 16:16:36 2003 +0100
+++ b/src/HOL/Datatype.thy	Thu Dec 04 21:57:15 2003 +0100
@@ -78,7 +78,7 @@
 subsection {* Finishing the datatype package setup *}
 
 text {* Belongs to theory @{text Datatype_Universe}; hides popular names. *}
-hide const Node Atom Leaf Numb Lim Split Case Suml Sumr
+hide const Push Node Atom Leaf Numb Lim Split Case Suml Sumr
 hide type node item