--- a/src/HOL/Nominal/Examples/SN.thy Wed Nov 15 15:39:22 2006 +0100
+++ b/src/HOL/Nominal/Examples/SN.thy Wed Nov 15 16:23:55 2006 +0100
@@ -92,7 +92,7 @@
show ?case
proof (simp)
have f: "\<exists>c::name. c\<sharp>(pi\<bullet>a,pi\<bullet>s1,pi\<bullet>s2,x)"
- by (rule at_exists_fresh[OF at_name_inst], simp add: fs_name1)
+ by (rule exists_fresh', simp add: fs_name1)
then obtain c::"name"
where f1: "c\<noteq>(pi\<bullet>a)" and f2: "c\<sharp>x" and f3: "c\<sharp>(pi\<bullet>s1)" and f4: "c\<sharp>(pi\<bullet>s2)"
by (force simp add: fresh_prod fresh_atm)
@@ -110,7 +110,7 @@
show ?case
proof (simp add: subst_eqvt)
have f: "\<exists>c::name. c\<sharp>(pi\<bullet>a,pi\<bullet>s1,pi\<bullet>s2,x)"
- by (rule at_exists_fresh[OF at_name_inst], simp add: fs_name1)
+ by (rule exists_fresh', simp add: fs_name1)
then obtain c::"name"
where f1: "c\<noteq>(pi\<bullet>a)" and f2: "c\<sharp>x" and f3: "c\<sharp>(pi\<bullet>s1)" and f4: "c\<sharp>(pi\<bullet>s2)"
by (force simp add: fresh_prod fresh_atm)
@@ -318,7 +318,7 @@
have k2: "((a,\<tau>)#\<Gamma>)\<turnstile>t:\<sigma>" by fact
have k3: "\<And>(pi::name prm) (x::'a::fs_name). P x (pi \<bullet>((a,\<tau>)#\<Gamma>)) (pi\<bullet>t) \<sigma>" by fact
have f: "\<exists>c::name. c\<sharp>(pi\<bullet>a,pi\<bullet>t,pi\<bullet>\<Gamma>,x)"
- by (rule at_exists_fresh[OF at_name_inst], simp add: fs_name1)
+ by (rule exists_fresh', simp add: fs_name1)
then obtain c::"name"
where f1: "c\<noteq>(pi\<bullet>a)" and f2: "c\<sharp>x" and f3: "c\<sharp>(pi\<bullet>t)" and f4: "c\<sharp>(pi\<bullet>\<Gamma>)"
by (force simp add: fresh_prod at_fresh[OF at_name_inst])