--- a/Nominal/Ex/Lambda.thy	Tue Apr 13 00:53:48 2010 +0200
+++ b/Nominal/Ex/Lambda.thy	Tue Apr 13 07:40:54 2010 +0200
@@ -260,15 +260,6 @@
 using a
 apply(induct)
 apply(tactic {* my_tac @{context} @{thms alpha_lam_raw.intros} 1 *})
-apply(tactic {* my_tac @{context} @{thms alpha_lam_raw.intros} 1 *})
-apply(perm_strict_simp)
-apply(rule alpha_lam_raw.intros)
-apply(simp)
-apply(perm_strict_simp)
-apply(rule alpha_lam_raw.intros)
-apply(simp add: alphas)
-apply(rule_tac p="- p" in permute_boolE)
-apply(perm_simp permute_minus_cancel(2))
 oops
 
 thm alpha_lam_raw.intros[no_vars]