--- a/src/HOL/Nominal/Examples/SOS.thy Thu Mar 03 22:06:15 2011 +0100
+++ b/src/HOL/Nominal/Examples/SOS.thy Fri Mar 04 00:09:47 2011 +0100
@@ -536,7 +536,7 @@
case (Var x \<Gamma> \<theta> T)
have "\<Gamma> \<turnstile> (Var x) : T" by fact
then have "(x,T)\<in>set \<Gamma>" by (cases) (auto simp add: trm.inject)
- with prems have "\<theta><Var x> \<Down> \<theta><Var x> \<and> \<theta><Var x>\<in> V T"
+ with Var have "\<theta><Var x> \<Down> \<theta><Var x> \<and> \<theta><Var x>\<in> V T"
by (auto intro!: Vs_reduce_to_themselves)
then show "\<exists>v. \<theta><Var x> \<Down> v \<and> v \<in> V T" by auto
qed