diff -r 0440bc1a2438 -r 14c7d7e29c44 Nominal/Ex/CPS/CPS3_DanvyFilinski.thy
--- a/Nominal/Ex/CPS/CPS3_DanvyFilinski.thy	Thu Jul 12 10:11:32 2012 +0100
+++ b/Nominal/Ex/CPS/CPS3_DanvyFilinski.thy	Sun Jul 15 13:03:47 2012 +0100
@@ -15,6 +15,7 @@
 | "atom c \<sharp> (x, M) \<Longrightarrow> (Lam x M)^l = l $$ (Lam x (Lam c (M^(c~))))"
   apply (simp only: eqvt_def CPS1_CPS2_graph_def)
   apply (rule, perm_simp, rule)
+  using [[simproc del: alpha_lst]]
   apply auto
   apply (case_tac x)
   apply (case_tac a)