--- a/Nominal/Term2.thy	Fri Feb 26 13:57:43 2010 +0100
+++ b/Nominal/Term2.thy	Fri Feb 26 15:10:55 2010 +0100
@@ -60,19 +60,19 @@
 *}
 print_theorems
 
-local_setup {* prove_const_rsp @{binding fv_rtrm2_rsp} [@{term fv_rtrm2}, @{term fv_rassign}]
+local_setup {* snd o prove_const_rsp @{binding fv_rtrm2_rsp} [@{term fv_rtrm2}, @{term fv_rassign}]
   (fn _ => fvbv_rsp_tac @{thm alpha_rtrm2_alpha_rassign.induct} @{thms fv_rtrm2_fv_rassign.simps} 1) *}
-local_setup {* prove_const_rsp @{binding rbv2_rsp} [@{term rbv2}]
+local_setup {* snd o prove_const_rsp @{binding rbv2_rsp} [@{term rbv2}]
   (fn _ => fvbv_rsp_tac @{thm alpha_rtrm2_alpha_rassign.inducts(2)} @{thms rbv2.simps} 1) *}
-local_setup {* prove_const_rsp @{binding rVr2_rsp} [@{term rVr2}]
+local_setup {* snd o prove_const_rsp @{binding rVr2_rsp} [@{term rVr2}]
   (fn _ => constr_rsp_tac @{thms alpha2_inj} @{thms fv_rtrm2_rsp} @{thms alpha2_equivp} 1) *}
-local_setup {* prove_const_rsp @{binding rAp2_rsp} [@{term rAp2}]
+local_setup {* snd o prove_const_rsp @{binding rAp2_rsp} [@{term rAp2}]
   (fn _ => constr_rsp_tac @{thms alpha2_inj} @{thms fv_rtrm2_rsp} @{thms alpha2_equivp} 1) *}
-local_setup {* prove_const_rsp @{binding rLm2_rsp} [@{term rLm2}]
+local_setup {* snd o prove_const_rsp @{binding rLm2_rsp} [@{term rLm2}]
   (fn _ => constr_rsp_tac @{thms alpha2_inj} @{thms fv_rtrm2_rsp} @{thms alpha2_equivp} 1) *}
-local_setup {* prove_const_rsp @{binding rLt2_rsp} [@{term rLt2}]
+local_setup {* snd o prove_const_rsp @{binding rLt2_rsp} [@{term rLt2}]
   (fn _ => constr_rsp_tac @{thms alpha2_inj} @{thms fv_rtrm2_rsp rbv2_rsp} @{thms alpha2_equivp} 1) *}
-local_setup {* prove_const_rsp @{binding permute_rtrm2_rsp} [@{term "permute :: perm \<Rightarrow> rtrm2 \<Rightarrow> rtrm2"}]
+local_setup {* snd o prove_const_rsp @{binding permute_rtrm2_rsp} [@{term "permute :: perm \<Rightarrow> rtrm2 \<Rightarrow> rtrm2"}]
   (fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha2_eqvt}) 1) *}
 
 end