--- a/Nominal/Term1.thy	Fri Feb 26 13:57:43 2010 +0100
+++ b/Nominal/Term1.thy	Fri Feb 26 15:10:55 2010 +0100
@@ -93,18 +93,17 @@
 *}
 print_theorems
 
-thm alpha_rtrm1_alpha_bp.induct
-local_setup {* prove_const_rsp @{binding fv_rtrm1_rsp} [@{term fv_rtrm1}]
+local_setup {* snd o prove_const_rsp @{binding fv_rtrm1_rsp} [@{term fv_rtrm1}]
   (fn _ => fvbv_rsp_tac @{thm alpha_rtrm1_alpha_bp.inducts(1)} @{thms fv_rtrm1_fv_bp.simps} 1) *}
-local_setup {* prove_const_rsp @{binding rVr1_rsp} [@{term rVr1}]
+local_setup {* snd o prove_const_rsp @{binding rVr1_rsp} [@{term rVr1}]
+  (fn _ => constr_rsp_tac @{thms alpha1_inj} @{thms fv_rtrm1_rsp} @{thms alpha1_equivp} 1) *}
+local_setup {* snd o prove_const_rsp @{binding rAp1_rsp} [@{term rAp1}]
   (fn _ => constr_rsp_tac @{thms alpha1_inj} @{thms fv_rtrm1_rsp} @{thms alpha1_equivp} 1) *}
-local_setup {* prove_const_rsp @{binding rAp1_rsp} [@{term rAp1}]
-  (fn _ => constr_rsp_tac @{thms alpha1_inj} @{thms fv_rtrm1_rsp} @{thms alpha1_equivp} 1) *}
-local_setup {* prove_const_rsp @{binding rLm1_rsp} [@{term rLm1}]
+local_setup {* snd o prove_const_rsp @{binding rLm1_rsp} [@{term rLm1}]
   (fn _ => constr_rsp_tac @{thms alpha1_inj} @{thms fv_rtrm1_rsp} @{thms alpha1_equivp} 1) *}
-local_setup {* prove_const_rsp @{binding rLt1_rsp} [@{term rLt1}]
+local_setup {* snd o prove_const_rsp @{binding rLt1_rsp} [@{term rLt1}]
   (fn _ => constr_rsp_tac @{thms alpha1_inj} @{thms fv_rtrm1_rsp} @{thms alpha1_equivp} 1) *}
-local_setup {* prove_const_rsp @{binding permute_rtrm1_rsp} [@{term "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1"}]
+local_setup {* snd o prove_const_rsp @{binding permute_rtrm1_rsp} [@{term "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1"}]
   (fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha1_eqvt}) 1) *}
 
 lemmas trm1_bp_induct = rtrm1_bp.induct[quot_lifted]