diff -r 72ad4e766acf -r 8aff3f3ce47f Nominal/Ex/SingleLet.thy
--- a/Nominal/Ex/SingleLet.thy	Sat May 22 13:51:47 2010 +0100
+++ b/Nominal/Ex/SingleLet.thy	Sun May 23 02:15:24 2010 +0100
@@ -5,7 +5,7 @@
 atom_decl name
 
 ML {* print_depth 50 *}
-declare [[STEPS = 4]]
+declare [[STEPS = 5]]
 
 
 nominal_datatype trm =
@@ -21,6 +21,8 @@
   "bn (As x t) = {atom x}"
 
 thm fv_trm_raw.simps[no_vars] fv_assg_raw.simps[no_vars] fv_bn_raw.simps[no_vars] bn_raw.simps[no_vars]
+thm alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros[no_vars]
+
 
 ML {* Inductive.the_inductive *}
 thm trm_assg.fv