diff -r 7c8783d2dcd0 -r d835a2771608 Nominal/Ex/SingleLet.thy
--- a/Nominal/Ex/SingleLet.thy	Mon Jun 21 15:41:59 2010 +0100
+++ b/Nominal/Ex/SingleLet.thy	Tue Jun 22 13:05:00 2010 +0100
@@ -4,8 +4,7 @@
 
 atom_decl name
 
-declare [[STEPS = 12]]
-
+declare [[STEPS = 13]]
 
 nominal_datatype trm =
   Var "name"
@@ -16,53 +15,11 @@
 | Bar x::"name" y::"name" t::"trm" bind y x in t x y
 | Baz x::"name" t1::"trm" t2::"trm" bind x in t1, bind x in t2 
 and assg =
-  As "name" "name" "trm" "name"
+  As "name" x::"name" t::"trm" bind x in t
 binder
   bn::"assg \<Rightarrow> atom set"
 where
-  "bn (As x y t z) = {atom x}"
-
-
-lemma
-  shows "alpha_trm_raw x x"
-  and "alpha_assg_raw y y"
-  and "alpha_bn_raw y y"
-apply(induct rule: trm_raw_assg_raw.inducts)
-apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros)
-apply(rule refl)
-apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros)
-apply(assumption)
-apply(assumption)
-apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros)
-apply(rule_tac x="0" in exI)
-apply(rule alpha_gen_refl)
-apply(assumption)
-apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros)
-apply(rule_tac x="0" in exI)
-apply(rule alpha_gen_refl)
-apply(assumption)
-apply(assumption)
-apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros)
-apply(rule_tac x="0" in exI)
-apply(rule alpha_gen_refl)
-apply(simp only: prod_alpha_def split_conv prod_rel.simps)
-apply(simp)
-apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros)
-apply(rule_tac x="0" in exI)
-apply(rule alpha_gen_refl)
-apply(simp only: prod_alpha_def split_conv prod_rel.simps)
-apply(simp)
-apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros)
-apply(rule refl)
-apply(rule refl)
-apply(assumption)
-apply(rule refl)
-apply(rule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros)
-apply(rule refl)
-apply(assumption)
-apply(rule refl)
-done
-
+  "bn (As x y t) = {atom x}"
 
 
 thm trm_assg.fv