diff -r a44479bde681 -r 017e33849f4d Nominal/Ex/Weakening.thy
--- a/Nominal/Ex/Weakening.thy	Tue Mar 22 12:18:30 2016 +0000
+++ b/Nominal/Ex/Weakening.thy	Thu Apr 19 13:57:17 2018 +0100
@@ -107,7 +107,7 @@
   valid2 :: "(name \<times> ty) fset \<Rightarrow> bool"
 where
   v2_Empty[intro]: "valid2 {||}"
-| v2_Insert[intro]: "\<lbrakk>(x, T) |\<notin>| Gamma; valid2 Gamma\<rbrakk> \<Longrightarrow> valid2 (insert_fset (x, T) Gamma)"
+| v2_Insert[intro]: "\<lbrakk>(x, T) |\<notin>| Gamma; valid2 Gamma\<rbrakk> \<Longrightarrow> valid2 (finsert (x, T) Gamma)"
 
 equivariance valid2
 
@@ -116,7 +116,7 @@
 where
     t2_Var[intro]: "\<lbrakk>valid2 \<Gamma>; (x, T) |\<in>| \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> 2\<turnstile> Var x : T"
   | t2_App[intro]: "\<lbrakk>\<Gamma> 2\<turnstile> t1 : T1 \<rightarrow> T2; \<Gamma> 2\<turnstile> t2 : T1\<rbrakk> \<Longrightarrow> \<Gamma> 2\<turnstile> App t1 t2 : T2"
-  | t2_Lam[intro]: "\<lbrakk>atom x \<sharp> \<Gamma>; insert_fset (x, T1) \<Gamma> 2\<turnstile> t : T2\<rbrakk> \<Longrightarrow> \<Gamma> 2\<turnstile> Lam [x]. t : T1 \<rightarrow> T2"
+  | t2_Lam[intro]: "\<lbrakk>atom x \<sharp> \<Gamma>; finsert (x, T1) \<Gamma> 2\<turnstile> t : T2\<rbrakk> \<Longrightarrow> \<Gamma> 2\<turnstile> Lam [x]. t : T1 \<rightarrow> T2"
 
 equivariance typing2
 
@@ -133,12 +133,8 @@
 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)
-apply(drule_tac x="xa" in meta_spec)
-apply(drule meta_mp)
-apply(simp add: fresh_at_base)
-apply(simp add: insert_fset_left_comm)
+apply(simp add: fresh_finsert fresh_ty)
+apply(force)
 done
 
 lemma weakening_version4: 
@@ -155,7 +151,7 @@
 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)
+apply(simp add: fresh_finsert)
 oops