--- a/src/HOL/List.thy Thu Mar 16 00:33:46 2000 +0100
+++ b/src/HOL/List.thy Thu Mar 16 00:35:27 2000 +0100
@@ -6,7 +6,7 @@
The datatype of finite lists.
*)
-List = Datatype + WF_Rel + NatBin +
+List = PreList +
datatype 'a list = Nil ("[]") | Cons 'a ('a list) (infixr "#" 65)