--- a/Nominal/Ex/Weakening.thy	Tue Feb 19 05:38:46 2013 +0000
+++ b/Nominal/Ex/Weakening.thy	Tue Feb 19 06:58:14 2013 +0000
@@ -49,7 +49,7 @@
 
 nominal_inductive typing
   avoids t_Lam: "x"
-  by (simp_all add: fresh_star_def fresh_ty)
+  by (simp_all add: fresh_star_def fresh_ty lam.fresh)
 
 
 abbreviation
@@ -122,7 +122,7 @@
 
 nominal_inductive typing2
   avoids t2_Lam: "x"
-  by (simp_all add: fresh_star_def fresh_ty)
+  by (simp_all add: fresh_star_def fresh_ty lam.fresh)
 
 lemma weakening_version3: 
   fixes \<Gamma>::"(name \<times> ty) fset"
@@ -133,7 +133,7 @@
 apply(nominal_induct \<Gamma> t T avoiding: x rule: typing2.strong_induct)
 apply(auto)[2]
 apply(rule t2_Lam)
-apply(simp add: fresh_insert_fset fresh_ty)
+apply(simp add: fresh_insert_fset fresh_Pair fresh_ty)
 apply(simp)
 apply(drule_tac x="xa" in meta_spec)
 apply(drule meta_mp)
@@ -141,24 +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 T')
-apply(auto)[2]
-apply(blast)
-apply(simp)
-apply(rule_tac ?'a="name" and x="(x, xa, t, T', \<Gamma>)" in obtain_fresh)
-apply(rule_tac t= "Lam [x]. t" and s="Lam [a]. ((a \<leftrightarrow> x) \<bullet> t)" in subst)
-defer
-apply(rule t2_Lam)
-apply(simp add: fresh_insert_fset)
-oops
-
-
 
 end