--- a/src/HOL/Induct/Comb.thy Tue Jun 30 20:50:34 1998 +0200
+++ b/src/HOL/Induct/Comb.thy Tue Jun 30 20:51:15 1998 +0200
@@ -13,7 +13,7 @@
*)
-Comb = Arith +
+Comb = Arith + Inductive +
(** Datatype definition of combinators S and K, with infixed application **)
datatype comb = K