diff -r 559419060d99 -r 278253330b6a Quot/Nominal/LamEx2.thy
--- a/Quot/Nominal/LamEx2.thy	Tue Feb 02 12:36:01 2010 +0100
+++ b/Quot/Nominal/LamEx2.thy	Tue Feb 02 12:48:12 2010 +0100
@@ -371,7 +371,7 @@
 lemma alpha_induct: 
   "\<lbrakk>qx = qxa; \<And>a b. a = b \<Longrightarrow> qxb (Var a) (Var b);
     \<And>x xa xb xc. \<lbrakk>x = xa; qxb x xa; xb = xc; qxb xb xc\<rbrakk> \<Longrightarrow> qxb (App x xb) (App xa xc);
- \<And>a t b s. \<exists>pi. ({atom a}, t) \<approx>gen \<lambda>x1 x2. x1 = x2 \<and> qxb x1 x2 fv pi ({atom b}, s) \<Longrightarrow> qxb (Lam a t) (Lam b s)\<rbrakk>
+ \<And>a t b s. \<exists>pi. ({atom a}, t) \<approx>gen (\<lambda>x1 x2. x1 = x2 \<and> qxb x1 x2) fv pi ({atom b}, s) \<Longrightarrow> qxb (Lam a t) (Lam b s)\<rbrakk>
     \<Longrightarrow> qxb qx qxa"
 unfolding alpha_gen by (lifting alpha.induct[unfolded alpha_gen])