# HG changeset patch
# User urbanc
# Date 1136995677 -3600
# Node ID 94782c7c42479475d0b357c579e1be953b1fc1ac
# Parent  7a00c80400b16ceeb511475c0af6e0cc534eaaa1
tuned proofs

diff -r 7a00c80400b1 -r 94782c7c4247 src/HOL/Nominal/Examples/SN.thy
--- a/src/HOL/Nominal/Examples/SN.thy	Wed Jan 11 14:00:11 2006 +0100
+++ b/src/HOL/Nominal/Examples/SN.thy	Wed Jan 11 17:07:57 2006 +0100
@@ -217,7 +217,7 @@
   shows   "valid (pi\<bullet>\<Gamma>)"
 using a
 apply(induct)
-apply(auto simp add: pt_fresh_bij[OF pt_name_inst, OF at_name_inst])
+apply(auto simp add: fresh_eqvt)
 done
 
 (* typing judgements *)
@@ -278,10 +278,10 @@
   moreover
   have "(pi\<bullet>(a,\<tau>))\<in>((pi::name prm)\<bullet>set \<Gamma>)" by (rule pt_set_bij2[OF pt_name_inst, OF at_name_inst])
   ultimately show "(pi\<bullet>\<Gamma>) \<turnstile> ((pi::name prm)\<bullet>Var a) : \<tau>"
-    using typing.intros by (force simp add: pt_list_set_pi[OF pt_name_inst, symmetric])
+    using typing.t1 by (force simp add: pt_list_set_pi[OF pt_name_inst, symmetric])
 next 
   case (t3 \<Gamma> \<sigma> \<tau> a t)
-  moreover have "(pi\<bullet>a)\<sharp>(pi\<bullet>\<Gamma>)" by (rule pt_fresh_bij1[OF pt_name_inst, OF at_name_inst])
+  moreover have "(pi\<bullet>a)\<sharp>(pi\<bullet>\<Gamma>)" by (simp add: fresh_eqvt)
   ultimately show "(pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>Lam [a].t) :\<tau>\<rightarrow>\<sigma>" by force 
 qed (auto)
 
diff -r 7a00c80400b1 -r 94782c7c4247 src/HOL/Nominal/Examples/Weakening.thy
--- a/src/HOL/Nominal/Examples/Weakening.thy	Wed Jan 11 14:00:11 2006 +0100
+++ b/src/HOL/Nominal/Examples/Weakening.thy	Wed Jan 11 17:07:57 2006 +0100
@@ -76,7 +76,7 @@
     using typing.intros by (force simp add: pt_list_set_pi[OF pt_name_inst, symmetric])
 next 
   case (t3 \<Gamma> \<sigma> \<tau> a t)
-  moreover have "(pi\<bullet>a)\<sharp>(pi\<bullet>\<Gamma>)" by (rule pt_fresh_bij1[OF pt_name_inst, OF at_name_inst])
+  moreover have "(pi\<bullet>a)\<sharp>(pi\<bullet>\<Gamma>)" by (simp add: fresh_eqvt)
   ultimately show "(pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>Lam [a].t) :\<tau>\<rightarrow>\<sigma>" by force 
 qed (auto)