# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1290741444 -32400
# Node ID dc988b07755ef2e5496273b04fce5fd8264818ad
# Parent  64abcfddb0c1a299b291acb305e6680a7b036fb1
missing freshness assumptions

diff -r 64abcfddb0c1 -r dc988b07755e Nominal/Ex/Foo2.thy
--- a/Nominal/Ex/Foo2.thy	Thu Nov 25 15:06:45 2010 +0900
+++ b/Nominal/Ex/Foo2.thy	Fri Nov 26 12:17:24 2010 +0900
@@ -277,8 +277,8 @@
   assumes a0: "\<And>name c. P1 c (Var name)"
   and a1: "\<And>trm1 trm2 c. \<lbrakk>\<And>d. P1 d trm1; \<And>d. P1 d trm2\<rbrakk> \<Longrightarrow> P1 c (App trm1 trm2)"
   and a2: "\<And>name trm c. (\<And>d. P1 d trm) \<Longrightarrow> P1 c (Lam name trm)"
-  and a3: "\<And>assg1 trm1 assg2 trm2 c. \<lbrakk>\<And>d. P2 c assg1; \<And>d. P1 d trm1; \<And>d. P2 d assg2; \<And>d. P1 d trm2\<rbrakk> \<Longrightarrow> P1 c (Let1 assg1 trm1 assg2 trm2)"
-  and a4: "\<And>name1 name2 trm1 trm2 c. \<lbrakk>\<And>d. P1 d trm1; \<And>d. P1 d trm2\<rbrakk> \<Longrightarrow> P1 c (Let2 name1 name2 trm1 trm2)"
+  and a3: "\<And>assg1 trm1 assg2 trm2 c. \<lbrakk>((set (bn assg1)) \<union> (set (bn assg2))) \<sharp>* c; \<And>d. P2 c assg1; \<And>d. P1 d trm1; \<And>d. P2 d assg2; \<And>d. P1 d trm2\<rbrakk> \<Longrightarrow> P1 c (Let1 assg1 trm1 assg2 trm2)"
+  and a4: "\<And>name1 name2 trm1 trm2 c. \<lbrakk>{atom name1, atom name2} \<sharp>* c; \<And>d. P1 d trm1; \<And>d. P1 d trm2\<rbrakk> \<Longrightarrow> P1 c (Let2 name1 name2 trm1 trm2)"
   and a5: "\<And>c. P2 c As_Nil"
   and a6: "\<And>name1 name2 trm assg c. \<lbrakk>\<And>d. P1 d trm; \<And>d. P2 d assg\<rbrakk> \<Longrightarrow> P2 c (As name1 name2 trm assg)"
   shows "P1 c trm" "P2 c assg"