--- a/Nominal/Term5.thy	Mon Mar 22 18:29:57 2010 +0100
+++ b/Nominal/Term5.thy	Mon Mar 22 18:38:59 2010 +0100
@@ -113,6 +113,7 @@
 apply (tactic {* (imp_elim_tac @{thms alpha_rtrm5.cases alpha_rlts.cases alpha_rbv5.cases} @{context}) 1 *})
 apply (simp_all add: alpha5_inj)
 apply (tactic {* eetac @{thm exi_sum} @{context} 1 *})
+(* HERE *)
 apply (simp add: alpha_gen)
 apply clarify
 apply(simp add: fresh_star_plus)