Nominal/Ex/TypeSchemes.thy
changeset 2886 d7066575cbb9
parent 2885 1264f2a21ea9
child 2950 0911cb7bf696
--- 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 *)