diff -r b9e4c812d2c6 -r 721d92623c9d Nominal/ExLet.thy
--- a/Nominal/ExLet.thy	Sat Mar 27 16:17:45 2010 +0100
+++ b/Nominal/ExLet.thy	Sat Mar 27 16:20:39 2010 +0100
@@ -7,7 +7,7 @@
 atom_decl name
 
 ML {* val _ = recursive := false  *}
-
+ML {* val _ = alpha_type := AlphaLst *}
 nominal_datatype trm =
   Vr "name"
 | Ap "trm" "trm"
@@ -19,8 +19,8 @@
 binder
   bn
 where
-  "bn Lnil = {}"
-| "bn (Lcons x t l) = {atom x} \<union> (bn l)"
+  "bn Lnil = []"
+| "bn (Lcons x t l) = (atom x) # (bn l)"
 
 thm trm_lts.fv
 thm trm_lts.eq_iff
@@ -29,7 +29,7 @@
 thm trm_lts.induct[no_vars]
 thm trm_lts.inducts[no_vars]
 thm trm_lts.distinct
-thm trm_lts.fv[simplified trm_lts.supp]
+thm trm_lts.fv[simplified trm_lts.supp(1-2)]
 
 primrec
   permute_bn_raw
@@ -80,7 +80,7 @@
   done
 
 lemma Lt_subst:
-  "supp (Abs (bn lts) trm) \<sharp>* q \<Longrightarrow> (Lt lts trm) = Lt (permute_bn q lts) (q \<bullet> trm)"
+  "supp (Abs_lst (bn lts) trm) \<sharp>* q \<Longrightarrow> (Lt lts trm) = Lt (permute_bn q lts) (q \<bullet> trm)"
   apply (simp only: trm_lts.eq_iff)
   apply (rule_tac x="q" in exI)
   apply (simp add: alphas)
@@ -98,7 +98,7 @@
 
 
 lemma fin_bn:
-  "finite (bn l)"
+  "finite (set (bn l))"
   apply(induct l rule: trm_lts.inducts(2))
   apply(simp_all add:permute_bn eqvts)
   done
@@ -110,7 +110,7 @@
   assumes a1: "\<And>name c. P1 c (Vr name)"
   and     a2: "\<And>trm1 trm2 c. \<lbrakk>\<And>d. P1 d trm1; \<And>d. P1 d trm2\<rbrakk> \<Longrightarrow> P1 c (Ap trm1 trm2)"
   and     a3: "\<And>name trm c. \<lbrakk>atom name \<sharp> c; \<And>d. P1 d trm\<rbrakk> \<Longrightarrow> P1 c (Lm name trm)"
-  and     a4: "\<And>lts trm c. \<lbrakk>bn lts \<sharp>* c; \<And>d. P2 d lts; \<And>d. P1 d trm\<rbrakk> \<Longrightarrow> P1 c (Lt lts trm)"
+  and     a4: "\<And>lts trm c. \<lbrakk>set (bn lts) \<sharp>* c; \<And>d. P2 d lts; \<And>d. P1 d trm\<rbrakk> \<Longrightarrow> P1 c (Lt lts trm)"
   and     a5: "\<And>c. P2 c Lnil"
   and     a6: "\<And>name trm lts c. \<lbrakk>\<And>d. P1 d trm; \<And>d. P2 d lts\<rbrakk> \<Longrightarrow> P2 c (Lcons name trm lts)"
   shows "P1 c t" and "P2 c l"
@@ -142,14 +142,14 @@
     apply(simp add: fresh_def)
     apply(simp add: trm_lts.fv[simplified trm_lts.supp])
     apply(simp)
-    apply(subgoal_tac "\<exists>q. (q \<bullet> bn (p \<bullet> lts)) \<sharp>* c \<and> supp (Abs (bn (p \<bullet> lts)) (p \<bullet> trm)) \<sharp>* q")
+    apply(subgoal_tac "\<exists>q. (q \<bullet> set (bn (p \<bullet> lts))) \<sharp>* c \<and> supp (Abs_lst (bn (p \<bullet> lts)) (p \<bullet> trm)) \<sharp>* q")
     apply(erule exE)
     apply(erule conjE)
     apply(subst Lt_subst)
     apply assumption
     apply(rule a4)
-    apply(simp add:perm_bn)
-    apply assumption
+    apply(simp add:perm_bn[symmetric])
+    apply(simp add: eqvts)
     apply (simp add: fresh_star_def fresh_def)
     apply(rotate_tac 1)
     apply(drule_tac x="q + p" in meta_spec)
@@ -157,8 +157,6 @@
     apply(rule at_set_avoiding2)
     apply(rule fin_bn)
     apply(simp add: finite_supp)
-    apply(simp add: supp_abs)
-    apply(rule finite_Diff)
     apply(simp add: finite_supp)
     apply(simp add: fresh_star_def fresh_def supp_abs)
     apply(simp add: eqvts permute_bn)
@@ -196,12 +194,10 @@
 
 
 lemma lets_not_ok1:
-  "(Lt (Lcons x (Vr x) (Lcons y (Vr y) Lnil)) (Ap (Vr x) (Vr y))) =
+  "x \<noteq> y \<Longrightarrow>
+   (Lt (Lcons x (Vr x) (Lcons y (Vr y) Lnil)) (Ap (Vr x) (Vr y))) \<noteq>
    (Lt (Lcons y (Vr x) (Lcons x (Vr y) Lnil)) (Ap (Vr x) (Vr y)))"
-  apply (simp add: alphas trm_lts.eq_iff)
-  apply (rule_tac x="0::perm" in exI)
-  apply (simp add: fresh_star_def eqvts)
-  apply blast
+  apply (simp add: alphas trm_lts.eq_iff fresh_star_def eqvts)
   done
 
 lemma lets_nok: