diff -r 1264f2a21ea9 -r d7066575cbb9 Nominal/Ex/TypeSchemes.thy --- a/Nominal/Ex/TypeSchemes.thy Wed Jun 22 12:18:22 2011 +0100 +++ b/Nominal/Ex/TypeSchemes.thy Wed Jun 22 13:40:25 2011 +0100 @@ -4,15 +4,6 @@ section {*** Type Schemes ***} -datatype foo = - Foo1 -| Foo2 bar -and bar = - Bar - -ML {* #induct (Datatype_Data.the_info @{theory} "TypeSchemes.bar") *} - - atom_decl name (* defined as a single nominal datatype *)