--- a/Nominal/Ex/Lambda.thy	Thu Dec 15 16:20:11 2011 +0000
+++ b/Nominal/Ex/Lambda.thy	Thu Dec 15 16:20:42 2011 +0000
@@ -169,7 +169,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 ::== (App (Var y) s)])"
   apply(simp add: eqvt_def subst'_graph_def)
-  apply (rule, perm_simp, rule)
+  apply(perm_simp, simp)
   apply(rule TrueI)
   apply(case_tac x)
   apply(rule_tac y="a" and c="(b, c)" in lam.strong_exhaust)