src/ZF/List.thy
changeset 810 91c68f74f458
parent 753 ec86863e87c8
child 1401 0c439768f45c
--- a/src/ZF/List.thy	Mon Dec 19 15:22:42 1994 +0100
+++ b/src/ZF/List.thy	Mon Dec 19 15:30:30 1994 +0100
@@ -10,7 +10,7 @@
 although complicating its derivation.
 *)
 
-List = "Datatype" + Univ + 
+List = Datatype + 
 
 consts
   "@"	     :: "[i,i]=>i"      			(infixr 60)