diff -r ca6ca6fc28af -r 25d11b449e92 Nominal/Ex/CPS/CPS1_Plotkin.thy
--- a/Nominal/Ex/CPS/CPS1_Plotkin.thy	Tue Aug 07 18:53:50 2012 +0100
+++ b/Nominal/Ex/CPS/CPS1_Plotkin.thy	Tue Aug 07 18:54:52 2012 +0100
@@ -10,8 +10,8 @@
 | "atom k \<sharp> (x, M) \<Longrightarrow> (Lam x M)* = Lam k (k~ $$ Lam x (M*))"
 | "atom k \<sharp> (M, N) \<Longrightarrow> atom m \<sharp> (N, k) \<Longrightarrow> atom n \<sharp> (k, m) \<Longrightarrow>
     (M $$ N)* = Lam k (M* $$ Lam m (N* $$ Lam n (m~ $$ n~ $$ k~)))"
-unfolding eqvt_def CPS_graph_def
-apply (rule, perm_simp, rule, rule)
+unfolding eqvt_def CPS_graph_aux_def
+apply (simp)
 using [[simproc del: alpha_lst]]
 apply (simp_all add: fresh_Pair_elim)
 apply (rule_tac y="x" in lt.exhaust)
@@ -80,8 +80,9 @@
   "(Var x)+ = Var x"
 | "(Lam x M)+ = Lam x (M*)"
 | "(M $$ N)+ = M $$ N"
-  unfolding convert_graph_def eqvt_def
-  apply (rule, perm_simp, rule, rule)
+  unfolding convert_graph_aux_def eqvt_def
+  apply (simp)
+  apply(rule TrueI)
   apply (erule lt.exhaust)
   using [[simproc del: alpha_lst]]
   apply (simp_all)
@@ -114,8 +115,8 @@
     Kapply (M $$ N) K = N; (Lam n (M+ $$ Var n $$ K))"
 | "\<not>isValue M \<Longrightarrow> atom m \<sharp> N \<Longrightarrow> atom m \<sharp> K \<Longrightarrow> atom n \<sharp> m \<Longrightarrow> atom n \<sharp> K \<Longrightarrow>
     Kapply (M $$ N) K = M; (Lam m (N*  $$ (Lam n (Var m $$ Var n $$ K))))"
-  unfolding Kapply_graph_def eqvt_def
-  apply (rule, perm_simp, rule, rule)
+  unfolding Kapply_graph_aux_def eqvt_def
+  apply (simp)
 using [[simproc del: alpha_lst]]
 apply (simp_all)
 apply (case_tac x)