diff -r 3641530002d6 -r 425b4c406d80 Nominal/Ex/CPS/Lt.thy
--- a/Nominal/Ex/CPS/Lt.thy	Sat Jun 09 19:48:19 2012 +0100
+++ b/Nominal/Ex/CPS/Lt.thy	Mon Jun 11 14:02:57 2012 +0100
@@ -17,7 +17,7 @@
 | "(App t1 t2)[y ::= s] = App (t1[y ::= s]) (t2[y ::= s])"
 | "atom x \<sharp> (y, s) \<Longrightarrow> (Lam x t)[y ::= s] = Lam x (t[y ::= s])"
   unfolding eqvt_def subst_graph_def
-  apply (rule, perm_simp, rule)
+  apply (simp)
   apply(rule TrueI)
   apply(auto simp add: lt.distinct lt.eq_iff)
   apply(rule_tac y="a" and c="(aa, b)" in lt.strong_exhaust)
@@ -25,9 +25,12 @@
   apply(simp_all add: fresh_star_def fresh_Pair_elim)
   apply blast
   apply (erule_tac c="(ya,sa)" in Abs_lst1_fcb2)
-  apply(simp_all add: Abs_fresh_iff)
+  apply(simp add: Abs_fresh_iff)
   apply(simp add: fresh_star_def fresh_Pair)
-  apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq)+
+  apply(simp add: eqvt_at_def)
+  apply(simp add: perm_supp_eq fresh_star_Pair)
+  apply(simp add: eqvt_at_def)
+  apply(simp add: perm_supp_eq fresh_star_Pair)
 done
 
 termination (eqvt) by lexicographic_order