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