--- a/Quot/Nominal/LFex.thy	Wed Feb 24 14:09:34 2010 +0100
+++ b/Quot/Nominal/LFex.thy	Wed Feb 24 14:37:51 2010 +0100
@@ -157,9 +157,12 @@
 
 end
 
-lemmas ALPHA_kind_ALPHA_ty_ALPHA_trm_inducts = alpha_rkind_alpha_rty_alpha_rtrm.inducts[unfolded alpha_gen, quot_lifted, folded alpha_gen]
+(*
+Lifts, but slow and not needed?.
+lemmas alpha_kind_alpha_ty_alpha_trm_induct = alpha_rkind_alpha_rty_alpha_rtrm.induct[unfolded alpha_gen, quot_lifted, folded alpha_gen]
+*)
 
-lemmas kind_ty_trm_INJECT = alpha_rkind_alpha_rty_alpha_rtrm_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen]
+lemmas kind_ty_trm_inj = alpha_rkind_alpha_rty_alpha_rtrm_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen]
 
 lemmas fv_kind_ty_trm = fv_rkind_fv_rty_fv_rtrm.simps[quot_lifted]
 
@@ -207,7 +210,7 @@
   "supp (APP M N) = supp M \<union> supp N"
   "supp rtrm = fv_trm rtrm \<Longrightarrow> supp (LAM rty name rtrm) = supp rty \<union> supp (Abs {atom name} rtrm)"
   apply(simp_all (no_asm) add: supp_def)
-  apply(simp_all only: kind_ty_trm_INJECT Abs_eq_iff alpha_gen)
+  apply(simp_all only: kind_ty_trm_inj Abs_eq_iff alpha_gen)
   apply(simp_all only: insert_eqvt empty_eqvt atom_eqvt supp_eqvt[symmetric] fv_eqvt[symmetric])
   apply(simp_all add: Collect_imp_eq Collect_neg_eq[symmetric] Set.Un_commute)
   apply(simp_all add: supp_at_base[simplified supp_def])