diff -r 1255ba99ed1e -r 74fb4f03bb51 src/HOL/Nominal/Examples/CK_Machine.thy
--- a/src/HOL/Nominal/Examples/CK_Machine.thy	Mon Jun 07 13:20:05 2010 +0200
+++ b/src/HOL/Nominal/Examples/CK_Machine.thy	Mon Jun 07 16:00:35 2010 +0200
@@ -492,7 +492,7 @@
   shows "(\<Delta>@\<Gamma>) \<turnstile> e[x::=e'] : T" 
 using a b 
 proof (nominal_induct \<Gamma>'\<equiv>"\<Delta>@[(x,T')]@\<Gamma>" e T avoiding: x e' \<Delta> rule: typing.strong_induct)
-  case (t_VAR \<Gamma>' y T x e' \<Delta>)
+  case (t_VAR y T x e' \<Delta>)
   then have a1: "valid (\<Delta>@[(x,T')]@\<Gamma>)" 
        and  a2: "(y,T) \<in> set (\<Delta>@[(x,T')]@\<Gamma>)" 
        and  a3: "\<Gamma> \<turnstile> e' : T'" by simp_all