--- a/Nominal/LFex.thy	Thu Mar 18 08:03:42 2010 +0100
+++ b/Nominal/LFex.thy	Thu Mar 18 08:32:55 2010 +0100
@@ -37,14 +37,14 @@
 
 lemma supp_eqs:
   "supp Type = {}"
-  "supp rkind = fv_kind rkind \<Longrightarrow> supp (KPi rty name rkind) = supp rty \<union> supp (Abs {atom name} rkind)"
+  "supp kind = fv_kind kind \<Longrightarrow> supp (KPi ty name kind) = supp ty \<union> supp (Abs {atom name} kind)"
   "supp (TConst i) = {atom i}"
   "supp (TApp A M) = supp A \<union> supp M"
-  "supp rty2 = fv_ty rty2 \<Longrightarrow> supp (TPi rty1 name rty2) = supp rty1 \<union> supp (Abs {atom name} rty2)"
+  "supp ty2 = fv_ty ty2 \<Longrightarrow> supp (TPi ty1 name ty2) = supp ty1 \<union> supp (Abs {atom name} ty2)"
   "supp (Const i) = {atom i}"
   "supp (Var x) = {atom x}"
   "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)"
+  "supp trm = fv_trm trm \<Longrightarrow> supp (Lam ty name trm) = supp ty \<union> supp (Abs {atom name} trm)"
   apply(simp_all (no_asm) add: supp_def permute_set_eq atom_eqvt kind_ty_trm_perm)
   apply(simp_all only: kind_ty_trm_eq_iff Abs_eq_iff alpha_gen)
   apply(simp_all only: ex_out)
@@ -64,7 +64,7 @@
   apply(simp_all add: supp_Abs)
   done
 
-lemma supp_rkind_rty_rtrm:
+lemma supp_kind_ty_trm:
   "supp Type = {}"
   "supp (KPi A x K) = supp A \<union> (supp K - {atom x})"
   "supp (TConst i) = {atom i}"