--- a/Tutorial/Lambda.thy	Thu Jul 12 10:11:32 2012 +0100
+++ b/Tutorial/Lambda.thy	Sun Jul 15 13:03:47 2012 +0100
@@ -41,6 +41,7 @@
 apply(simp add: eqvt_def height_graph_def)
 apply(rule TrueI)
 apply(rule_tac y="x" in lam.exhaust)
+using [[simproc del: alpha_lst]]
 apply(auto)
 apply(erule_tac c="()" in Abs_lst1_fcb2)
 apply(simp_all add: fresh_def pure_supp eqvt_at_def fresh_star_def)
@@ -61,6 +62,7 @@
   unfolding eqvt_def subst_graph_def
   apply(rule, perm_simp, rule)
   apply(rule TrueI)
+  using [[simproc del: alpha_lst]]
   apply(auto)
   apply(rule_tac y="a" and c="(aa, b)" in lam.strong_exhaust)
   apply(blast)+