src/HOL/PreList.thy

--- a/src/HOL/PreList.thy	Fri Nov 24 14:09:09 2000 +0100
+++ b/src/HOL/PreList.thy	Fri Nov 24 16:49:27 2000 +0100
@@ -1,4 +1,4 @@
-(*  Title:      HOL/List.thy
+(*  Title:      HOL/PreList.thy
     ID:         $Id$
     Author:     Tobias Nipkow
     Copyright   2000 TU Muenchen
@@ -17,4 +17,7 @@
 (*belongs to theory Wellfounded_Recursion*)
 declare wf_induct [induct set: wf]
 
+(*belongs to theory Datatype_Universe; hides popular names *)
+hide const Node Atom Leaf Numb Lim Funs Split Case
+
 end