diff -r a1d27083e688 -r 1785a111c2b6 Nominal/Ex/Lambda.thy
--- a/Nominal/Ex/Lambda.thy	Tue May 18 15:58:52 2010 +0200
+++ b/Nominal/Ex/Lambda.thy	Tue May 18 17:06:21 2010 +0200
@@ -521,7 +521,7 @@
   qed
 
 lemma simp3:
-  "x \<noteq> y \<Longrightarrow> atom x \<notin> fv_lam_raw s \<Longrightarrow> Lam_raw x (subst_raw t y s) = Lam_raw x (subst_raw t y s)"
+  "x \<noteq> y \<Longrightarrow> atom x \<notin> fv_lam_raw s \<Longrightarrow> subst_raw (Lam_raw x t) y s = Lam_raw x (subst_raw t y s)"
   by simp
 
 lemmas subst_simps = subst_raw.simps(1-2)[quot_lifted,no_vars]