--- a/Nominal/Ex/CPS/CPS3_DanvyFilinski.thy	Tue Aug 07 18:53:50 2012 +0100
+++ b/Nominal/Ex/CPS/CPS3_DanvyFilinski.thy	Tue Aug 07 18:54:52 2012 +0100
@@ -13,8 +13,7 @@
 | "(x~)^l = l $$ (x~)"
 | "(M$$N)^l = M*(%m. (N*(%n.((m $$ n) $$ l))))"
 | "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)
+  apply (simp add: eqvt_def CPS1_CPS2_graph_aux_def)
   using [[simproc del: alpha_lst]]
   apply auto
   apply (case_tac x)