--- a/src/HOL/Nominal/Examples/Weakening.thy Fri Jun 30 18:26:36 2006 +0200
+++ b/src/HOL/Nominal/Examples/Weakening.thy Sun Jul 02 17:27:10 2006 +0200
@@ -42,7 +42,7 @@
shows "valid (pi\<bullet>\<Gamma>)"
using a
apply(induct)
-apply(auto simp add: fresh_eqvt)
+apply(auto simp add: fresh_bij)
done
(* typing judgements *)
@@ -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 (simp add: fresh_eqvt)
+ moreover have "(pi\<bullet>a)\<sharp>(pi\<bullet>\<Gamma>)" by (simp add: fresh_bij)
ultimately show "(pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>Lam [a].t) :\<tau>\<rightarrow>\<sigma>" by force
qed (auto)