--- a/Nominal/ExLetRec.thy	Mon Mar 29 00:30:20 2010 +0200
+++ b/Nominal/ExLetRec.thy	Mon Mar 29 00:30:47 2010 +0200
@@ -2,11 +2,13 @@
 imports "Parser"
 begin
 
+
 text {* example 3 or example 5 from Terms.thy *}
 
 atom_decl name
 
 ML {* val _ = recursive := true *}
+ML {* val _ = alpha_type := AlphaLst *}
 nominal_datatype trm =
   Vr "name"
 | Ap "trm" "trm"
@@ -18,8 +20,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
@@ -27,6 +29,7 @@
 thm trm_lts.perm
 thm trm_lts.induct
 thm trm_lts.distinct
+thm trm_lts.supp
 thm trm_lts.fv[simplified trm_lts.supp]
 
 (* why is this not in HOL simpset? *)
@@ -35,14 +38,13 @@
 
 lemma lets_bla:
   "x \<noteq> z \<Longrightarrow> y \<noteq> z \<Longrightarrow> x \<noteq> y \<Longrightarrow>(Lt (Lcons x (Vr y) Lnil) (Vr x)) \<noteq> (Lt (Lcons x (Vr z) Lnil) (Vr x))"
-  apply (simp add: trm_lts.eq_iff alpha_gen2 set_sub)
-  done
+  by (simp add: trm_lts.eq_iff alphas2 set_sub)
 
 lemma lets_ok:
   "(Lt (Lcons x (Vr x) Lnil) (Vr x)) = (Lt (Lcons y (Vr y) Lnil) (Vr y))"
   apply (simp add: trm_lts.eq_iff)
   apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
-  apply (simp_all add: alpha_gen2 fresh_star_def eqvts)
+  apply (simp_all add: alphas2 fresh_star_def eqvts)
   done
 
 lemma lets_ok3:
@@ -67,6 +69,13 @@
   apply (simp add: alphas trm_lts.eq_iff fresh_star_def)
   done
 
+lemma lets_ok4:
+  "(Lt (Lcons x (Ap (Vr y) (Vr x)) (Lcons y (Vr y) Lnil)) (Ap (Vr x) (Vr y))) =
+   (Lt (Lcons y (Ap (Vr x) (Vr y)) (Lcons x (Vr x) Lnil)) (Ap (Vr y) (Vr x)))"
+  apply (simp add: alphas trm_lts.eq_iff)
+  apply (rule_tac x="(x \<leftrightarrow> y)" in exI)
+  apply (simp add: atom_eqvt fresh_star_def)
+  done
 
 end