# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1274195181 -7200
# Node ID 1785a111c2b674b0b6a6fca984d5641b81a530e0
# Parent  a1d27083e68830ac355a4bb20be5ffeb88df14ce
subst fix

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]