--- a/Nominal/Ex/ExLet.thy	Tue May 04 07:22:33 2010 +0100
+++ b/Nominal/Ex/ExLet.thy	Tue May 04 11:08:30 2010 +0200
@@ -1,17 +1,15 @@
 theory ExLet
-imports "../Parser" "../../Attic/Prove"
+imports "../NewParser" "../../Attic/Prove"
 begin
 
 text {* example 3 or example 5 from Terms.thy *}
 
 atom_decl name
 
-ML {* val _ = recursive := false *}
-ML {* val _ = alpha_type := AlphaLst *}
 nominal_datatype trm =
   Vr "name"
 | Ap "trm" "trm"
-| Lm x::"name" t::"trm"  bind x in t
+| Lm x::"name" t::"trm"  bind_set x in t
 | Lt a::"lts" t::"trm"   bind "bn a" in t
 (*| L a::"lts" t1::"trm" t2::"trm"  bind "bn a" in t1, bind "bn a" in t2*)
 and lts =
@@ -52,11 +50,10 @@
   apply simp
   apply clarify
   apply (erule alpha_trm_raw_alpha_lts_raw_alpha_bn_raw.inducts)
+  apply (rule TrueI)+
   apply simp_all
-  apply (rule alpha_trm_raw_alpha_lts_raw_alpha_bn_raw.intros)
-  apply simp
-  apply (rule alpha_trm_raw_alpha_lts_raw_alpha_bn_raw.intros)
-  apply simp
+  apply (rule_tac [!] alpha_trm_raw_alpha_lts_raw_alpha_bn_raw.intros)
+  apply simp_all
   done
 
 lemmas permute_bn = permute_bn_raw.simps[quot_lifted]
@@ -64,8 +61,8 @@
 lemma permute_bn_zero:
   "permute_bn 0 a = a"
   apply(induct a rule: trm_lts.inducts(2))
-  apply(rule TrueI)
-  apply(simp_all add:permute_bn eqvts)
+  apply(rule TrueI)+
+  apply(simp_all add:permute_bn)
   done
 
 lemma permute_bn_add:
@@ -74,37 +71,29 @@
 
 lemma permute_bn_alpha_bn: "alpha_bn lts (permute_bn q lts)"
   apply(induct lts rule: trm_lts.inducts(2))
-  apply(rule TrueI)
+  apply(rule TrueI)+
   apply(simp_all add:permute_bn eqvts trm_lts.eq_iff)
   done
 
 lemma perm_bn:
   "p \<bullet> bn l = bn(permute_bn p l)"
   apply(induct l rule: trm_lts.inducts(2))
-  apply(rule TrueI)
+  apply(rule TrueI)+
   apply(simp_all add:permute_bn eqvts)
   done
 
 lemma fv_perm_bn:
   "fv_bn l = fv_bn (permute_bn p l)"
   apply(induct l rule: trm_lts.inducts(2))
-  apply(rule TrueI)
+  apply(rule TrueI)+
   apply(simp_all add:permute_bn eqvts)
   done
 
-lemma fv_fv_bn:
-  "fv_bn l - set (bn l) = fv_lts l - set (bn l)"
-  apply(induct l rule: trm_lts.inducts(2))
-  apply(rule TrueI)
-  apply(simp_all add:permute_bn eqvts)
-  by blast
-
 lemma Lt_subst:
   "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 (simp add: trm_lts.eq_iff permute_bn_alpha_bn)
   apply (rule_tac x="q" in exI)
   apply (simp add: alphas)
-  apply (simp add: permute_bn_alpha_bn)
   apply (simp add: perm_bn[symmetric])
   apply (simp add: eqvts[symmetric])
   apply (simp add: supp_abs)
@@ -204,8 +193,7 @@
   "(Lt (Lcons x (Vr y) 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: alphas)
-  apply (simp add: fresh_star_def eqvts)
+  apply (simp_all add: alphas eqvts supp_at_base fresh_star_def)
   done
 
 lemma lets_ok3: