diff -r b4404b13f775 -r 37c0d7953cba Nominal/Ex/Let.thy --- a/Nominal/Ex/Let.thy Wed Jun 29 17:01:09 2011 +0100 +++ b/Nominal/Ex/Let.thy Wed Jun 29 19:21:26 2011 +0100 @@ -2,6 +2,7 @@ imports "../Nominal2" begin + atom_decl name nominal_datatype trm = @@ -305,6 +306,7 @@ apply (erule alpha_bn_inducts) oops + end