diff -r 6eacf60ce41d -r 8814494fe4da Nominal/LFex.thy
--- a/Nominal/LFex.thy	Fri Feb 26 13:57:43 2010 +0100
+++ b/Nominal/LFex.thy	Fri Feb 26 15:10:55 2010 +0100
@@ -91,24 +91,24 @@
  |> snd o (Quotient_Def.quotient_lift_const ("fv_trm", @{term fv_rtrm}))) *}
 print_theorems
 
-local_setup {* prove_const_rsp @{binding rfv_rsp} [@{term fv_rkind}, @{term fv_rty}, @{term fv_rtrm}]
+local_setup {* snd o prove_const_rsp @{binding rfv_rsp} [@{term fv_rkind}, @{term fv_rty}, @{term fv_rtrm}]
   (fn _ => fvbv_rsp_tac @{thm alpha_rkind_alpha_rty_alpha_rtrm.induct} @{thms fv_rkind_fv_rty_fv_rtrm.simps} 1) *}
-local_setup {* prove_const_rsp Binding.empty [@{term "permute :: perm \<Rightarrow> rkind \<Rightarrow> rkind"}]
+local_setup {* snd o prove_const_rsp Binding.empty [@{term "permute :: perm \<Rightarrow> rkind \<Rightarrow> rkind"}]
   (fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha_eqvt}) 1) *}
-local_setup {* prove_const_rsp Binding.empty [@{term "permute :: perm \<Rightarrow> rty \<Rightarrow> rty"}]
+local_setup {* snd o prove_const_rsp Binding.empty [@{term "permute :: perm \<Rightarrow> rty \<Rightarrow> rty"}]
   (fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha_eqvt}) 1) *}
-local_setup {* prove_const_rsp Binding.empty [@{term "permute :: perm \<Rightarrow> rtrm \<Rightarrow> rtrm"}]
+local_setup {* snd o prove_const_rsp Binding.empty [@{term "permute :: perm \<Rightarrow> rtrm \<Rightarrow> rtrm"}]
   (fn _ => asm_simp_tac (HOL_ss addsimps @{thms alpha_eqvt}) 1) *}
 ML {* fun const_rsp_tac _ = constr_rsp_tac @{thms alpha_rkind_alpha_rty_alpha_rtrm_inj}
   @{thms rfv_rsp} @{thms alpha_equivps} 1 *}
-local_setup {* prove_const_rsp Binding.empty [@{term TConst}] const_rsp_tac *}
-local_setup {* prove_const_rsp Binding.empty [@{term TApp}] const_rsp_tac *}
-local_setup {* prove_const_rsp Binding.empty [@{term Var}] const_rsp_tac *}
-local_setup {* prove_const_rsp Binding.empty [@{term App}] const_rsp_tac *}
-local_setup {* prove_const_rsp Binding.empty [@{term Const}] const_rsp_tac *}
-local_setup {* prove_const_rsp Binding.empty [@{term KPi}] const_rsp_tac *}
-local_setup {* prove_const_rsp Binding.empty [@{term TPi}] const_rsp_tac *}
-local_setup {* prove_const_rsp Binding.empty [@{term Lam}] const_rsp_tac *}
+local_setup {* snd o prove_const_rsp Binding.empty [@{term TConst}] const_rsp_tac *}
+local_setup {* snd o prove_const_rsp Binding.empty [@{term TApp}] const_rsp_tac *}
+local_setup {* snd o prove_const_rsp Binding.empty [@{term Var}] const_rsp_tac *}
+local_setup {* snd o prove_const_rsp Binding.empty [@{term App}] const_rsp_tac *}
+local_setup {* snd o prove_const_rsp Binding.empty [@{term Const}] const_rsp_tac *}
+local_setup {* snd o prove_const_rsp Binding.empty [@{term KPi}] const_rsp_tac *}
+local_setup {* snd o prove_const_rsp Binding.empty [@{term TPi}] const_rsp_tac *}
+local_setup {* snd o prove_const_rsp Binding.empty [@{term Lam}] const_rsp_tac *}
 
 lemmas kind_ty_trm_induct = rkind_rty_rtrm.induct[quot_lifted]