diff -r 886655a150f6 -r d1b97708d5eb src/HOL/Nominal/Examples/LocalWeakening.thy
--- a/src/HOL/Nominal/Examples/LocalWeakening.thy	Thu Jun 21 20:48:48 2007 +0200
+++ b/src/HOL/Nominal/Examples/LocalWeakening.thy	Thu Jun 21 22:10:16 2007 +0200
@@ -170,7 +170,7 @@
   ultimately show "\<Gamma>2 \<turnstile> lPar x : T" by auto
 next
   case (t_lLam x t T1 \<Gamma>1 T2 \<Gamma>2) (* lambda case *)
-  have vc: "x\<sharp>\<Gamma>2" "x\<sharp>t" by fact  (* variable convention *)
+  have vc: "x\<sharp>\<Gamma>2" "x\<sharp>t" by fact+  (* variable convention *)
   have ih: "\<lbrakk>(x,T1)#\<Gamma>1 \<subseteq> (x,T1)#\<Gamma>2; valid ((x,T1)#\<Gamma>2)\<rbrakk> \<Longrightarrow> (x,T1)#\<Gamma>2 \<turnstile> freshen t x : T2" by fact
   have "\<Gamma>1 \<subseteq> \<Gamma>2" by fact
   then have "(x,T1)#\<Gamma>1 \<subseteq> (x,T1)#\<Gamma>2" by simp