--- a/Nominal/ExLetRec.thy	Sat Mar 27 16:17:45 2010 +0100
+++ b/Nominal/ExLetRec.thy	Sat Mar 27 16:20:39 2010 +0100
@@ -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? *)
@@ -66,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