--- 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)

--- a/Nominal/Nominal2.thy	Sun Sep 05 06:42:53 2010 +0800
+++ b/Nominal/Nominal2.thy	Sun Sep 05 07:00:19 2010 +0800
@@ -539,6 +539,8 @@
       ||>> lift_thms qtys [] raw_exhaust_thms
     else raise TEST lthyA
 
+  val qinducts = Project_Rule.projections lthyA qinduct
+
   (* supports lemmas *) 
   val qsupports_thms =
     if get_STEPS lthy > 28
@@ -573,6 +575,7 @@
      ||>> Local_Theory.note ((thms_suffix "fv_bn_eqvt", []), qfv_qbn_eqvts) 
      ||>> Local_Theory.note ((thms_suffix "size_eqvt", []), qsize_eqvt)
      ||>> Local_Theory.note ((thms_suffix "induct", []), [qinduct]) 
+     ||>> Local_Theory.note ((thms_suffix "inducts", []), qinducts) 
      ||>> Local_Theory.note ((thms_suffix "exhaust", []), qexhausts)
      ||>> Local_Theory.note ((thms_suffix "supports", []), qsupports_thms)
      ||>> Local_Theory.note ((thms_suffix "fsupp", []), qfsupp_thms)