diff -r e46d4ee64221 -r 1b7c034c9e9e Nominal/Ex/Weakening.thy
--- a/Nominal/Ex/Weakening.thy	Tue Jun 12 14:22:58 2012 +0100
+++ b/Nominal/Ex/Weakening.thy	Mon Jun 18 14:50:02 2012 +0100
@@ -49,7 +49,7 @@
 
 nominal_inductive typing
   avoids t_Lam: "x"
-  by (simp_all add: fresh_star_def fresh_ty lam.fresh)
+  by (simp_all add: fresh_star_def fresh_ty)
 
 
 abbreviation
@@ -122,7 +122,7 @@
 
 nominal_inductive typing2
   avoids t2_Lam: "x"
-  by (simp_all add: fresh_star_def fresh_ty lam.fresh)
+  by (simp_all add: fresh_star_def fresh_ty)
 
 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_Pair fresh_ty)
+apply(simp add: fresh_insert_fset fresh_ty)
 apply(simp)
 apply(drule_tac x="xa" in meta_spec)
 apply(drule meta_mp)
@@ -147,11 +147,19 @@
   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(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