--- a/Nominal/Ex/SingleLet.thy	Sun Sep 05 06:42:53 2010 +0800
+++ b/Nominal/Ex/SingleLet.thy	Sun Sep 05 07:00:19 2010 +0800
@@ -1,5 +1,5 @@
 theory SingleLet
-imports "../Nominal2" "../Abs"
+imports "../Nominal2" 
 begin
 
 atom_decl name
@@ -24,6 +24,7 @@
 
 thm single_let.distinct
 thm single_let.induct
+thm single_let.inducts
 thm single_let.exhaust
 thm single_let.fv_defs
 thm single_let.bn_defs
@@ -45,8 +46,8 @@
 
 
 lemma supp_fv:
-  "fv_trm t = supp t \<and> fv_assg as = supp as \<and> fv_bn as = supp_rel alpha_bn as"
-apply(rule single_let.induct)
+  "fv_trm t = supp t" "fv_assg as = supp as" "fv_bn as = supp_rel alpha_bn as"
+apply(induct t and as rule: single_let.inducts)
 -- " 0A "
 apply(simp only: single_let.fv_defs supp_Pair[symmetric])
 apply(simp only: supp_abs(3)[symmetric])?
@@ -70,7 +71,6 @@
 apply(drule test2)
 apply(simp only:)
 -- " 2 "
-apply(erule conjE)+
 apply(simp only: single_let.fv_defs supp_Pair[symmetric])
 apply(simp only: supp_abs(3)[symmetric])
 apply(simp (no_asm) only: supp_def supp_rel_def)
@@ -109,7 +109,6 @@
 apply(drule test2)+
 apply(simp only: supp_Pair Un_assoc conj_assoc)
 -- "last"
-apply(rule conjI)
 apply(simp only: single_let.fv_defs supp_Pair[symmetric])
 apply(simp only: supp_abs(3)[symmetric])
 apply(simp (no_asm) only: supp_def supp_rel_def)