--- a/Nominal/Ex/CPS/CPS2_DanvyNielsen.thy	Thu Jul 12 10:11:32 2012 +0100
+++ b/Nominal/Ex/CPS/CPS2_DanvyNielsen.thy	Sun Jul 15 13:03:47 2012 +0100
@@ -18,8 +18,10 @@
 | fill_abs  : "atom x \<sharp> M \<Longrightarrow> (CAbs x C)<M> = Lam x (C<M>)"
   unfolding eqvt_def fill_graph_def
   apply perm_simp
+  using [[simproc del: alpha_lst]]
   apply auto
   apply (rule_tac y="a" and c="b" in cpsctxt.strong_exhaust)
+  using [[simproc del: alpha_lst]]
   apply (auto simp add: fresh_star_def)
   apply (erule Abs_lst1_fcb)
   apply (simp_all add: Abs_fresh_iff)[2]
@@ -41,8 +43,10 @@
 | "ccomp (CFun C N) C'  = CFun (ccomp C C') N"
   unfolding eqvt_def ccomp_graph_def
   apply perm_simp
+  using [[simproc del: alpha_lst]]
   apply auto
   apply (rule_tac y="a" and c="b" in cpsctxt.strong_exhaust)
+  using [[simproc del: alpha_lst]]
   apply (auto simp add: fresh_star_def)
   apply blast+
   apply (erule Abs_lst1_fcb)
@@ -71,10 +75,12 @@
      ccomp (CPS M) (CAbs a (CArg (Var a $$ (CPSv N)) Hole))"
 | "~isValue M \<Longrightarrow> ~isValue N \<Longrightarrow> atom a \<sharp> (N, b) \<Longrightarrow> CPS (M $$ N) =
      ccomp (CPS M) (CAbs a (ccomp (CPS N) (CAbs b (CArg (Var a $$ Var b) Hole))))"
+  using [[simproc del: alpha_lst]]
   apply auto
   defer
   apply (case_tac x)
   apply (rule_tac y="a" in lt.exhaust)
+  using [[simproc del: alpha_lst]]
   apply auto
   apply blast
   apply (rule_tac x="lt" and ?'a="name" in obtain_fresh)