--- 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)