--- a/Nominal/Ex/CPS/CPS2_DanvyNielsen.thy	Tue Aug 07 18:53:50 2012 +0100
+++ b/Nominal/Ex/CPS/CPS2_DanvyNielsen.thy	Tue Aug 07 18:54:52 2012 +0100
@@ -16,8 +16,8 @@
 | fill_fun  : "(CFun C N)<M> = (C<M>) $$ N"
 | fill_arg  : "(CArg N C)<M> = N $$ (C<M>)"
 | fill_abs  : "atom x \<sharp> M \<Longrightarrow> (CAbs x C)<M> = Lam x (C<M>)"
-  unfolding eqvt_def fill_graph_def
-  apply perm_simp
+  unfolding eqvt_def fill_graph_aux_def
+  apply simp
   using [[simproc del: alpha_lst]]
   apply auto
   apply (rule_tac y="a" and c="b" in cpsctxt.strong_exhaust)
@@ -41,8 +41,8 @@
 | "atom x \<sharp> C' \<Longrightarrow> ccomp (CAbs x C) C' = CAbs x (ccomp C C')"
 | "ccomp (CArg N C) C' = CArg N (ccomp C C')"
 | "ccomp (CFun C N) C'  = CFun (ccomp C C') N"
-  unfolding eqvt_def ccomp_graph_def
-  apply perm_simp
+  unfolding eqvt_def ccomp_graph_aux_def
+  apply simp
   using [[simproc del: alpha_lst]]
   apply auto
   apply (rule_tac y="a" and c="b" in cpsctxt.strong_exhaust)