--- a/src/HOL/Induct/Sexp.thy Thu Oct 12 18:09:06 2000 +0200
+++ b/src/HOL/Induct/Sexp.thy Thu Oct 12 18:38:23 2000 +0200
@@ -7,7 +7,7 @@
structures by hand.
*)
-Sexp = Univ + Inductive +
+Sexp = Datatype_Universe + Inductive +
consts
sexp :: 'a item set