diff -r 6061ae1f90f2 -r 9bc16273c2d4 src/HOL/Induct/Sexp.thy
--- a/src/HOL/Induct/Sexp.thy	Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Induct/Sexp.thy	Fri Jun 17 16:12:49 2005 +0200
@@ -7,7 +7,7 @@
 structures by hand.
 *)
 
-theory Sexp = Datatype_Universe + Inductive:
+theory Sexp imports Datatype_Universe Inductive begin
 consts
   sexp      :: "'a item set"