--- a/Nominal/Ex/Weakening.thy	Sat Dec 17 17:03:01 2011 +0000
+++ b/Nominal/Ex/Weakening.thy	Sat Dec 17 17:08:47 2011 +0000
@@ -141,16 +141,6 @@
 apply(simp add: insert_fset_left_comm)
 done
 
-lemma weakening_version4: 
-  fixes \<Gamma>::"(name \<times> ty) fset"
-  assumes a: "\<Gamma> 2\<turnstile> t : T" 
-  and     b: "(x, T') |\<notin>| \<Gamma>"
-  shows "{|(x, T')|} |\<union>| \<Gamma> 2\<turnstile> t : T"
-using a b
-apply(induct \<Gamma> t T arbitrary: x)
-apply(auto)[2]
-apply(rule t2_Lam)
-oops
 
 end