diff -r 0440bc1a2438 -r 14c7d7e29c44 Nominal/Ex/CPS/CPS1_Plotkin.thy
--- a/Nominal/Ex/CPS/CPS1_Plotkin.thy	Thu Jul 12 10:11:32 2012 +0100
+++ b/Nominal/Ex/CPS/CPS1_Plotkin.thy	Sun Jul 15 13:03:47 2012 +0100
@@ -12,10 +12,12 @@
     (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)
+using [[simproc del: alpha_lst]]
 apply (simp_all add: fresh_Pair_elim)
 apply (rule_tac y="x" in lt.exhaust)
 apply (auto)[3]
 apply (rule_tac x="name" and ?'a="name" in obtain_fresh)
+using [[simproc del: alpha_lst]]
 apply (simp_all add: fresh_at_base)[3]
 apply (rule_tac x="(lt1, lt2)" and ?'a="name" in obtain_fresh)
 apply (rule_tac x="(lt2, a)" and ?'a="name" in obtain_fresh)
@@ -81,6 +83,7 @@
   unfolding convert_graph_def eqvt_def
   apply (rule, perm_simp, rule, rule)
   apply (erule lt.exhaust)
+  using [[simproc del: alpha_lst]]
   apply (simp_all)
   apply blast
   apply (simp add: Abs1_eq_iff CPS.eqvt)
@@ -113,6 +116,7 @@
     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)
+using [[simproc del: alpha_lst]]
 apply (simp_all)
 apply (case_tac x)
 apply (rule_tac y="a" in lt.exhaust)