--- a/src/ZF/ex/LList.thy Mon Dec 19 15:22:42 1994 +0100
+++ b/src/ZF/ex/LList.thy Mon Dec 19 15:30:30 1994 +0100
@@ -14,7 +14,7 @@
a typing rule for it, based on some notion of "productivity..."
*)
-LList = QUniv + "Datatype" +
+LList = Datatype +
consts
llist :: "i=>i"