--- 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