diff -r 20d4899f5d48 -r ade64af4c57c 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