--- a/src/ZF/ex/Comb.thy Mon Dec 19 15:22:42 1994 +0100
+++ b/src/ZF/ex/Comb.thy Mon Dec 19 15:30:30 1994 +0100
@@ -13,7 +13,7 @@
*)
-Comb = Univ + "Datatype" +
+Comb = Datatype +
(** Datatype definition of combinators S and K, with infixed application **)
consts comb :: "i"