diff -r b52b72676e20 -r 76fa21f27f22 Nominal/LFex.thy
--- a/Nominal/LFex.thy	Thu Mar 18 14:48:27 2010 +0100
+++ b/Nominal/LFex.thy	Thu Mar 18 15:13:20 2010 +0100
@@ -46,7 +46,7 @@
   "supp (App M N) = supp M \<union> supp N"
   "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)
-  apply(simp_all only: kind_ty_trm_eq_iff Abs_eq_iff alpha_gen)
+  apply(simp_all only: kind_ty_trm.eq_iff Abs_eq_iff alpha_gen)
   apply(simp_all only: ex_out)
   apply(simp_all only: eqvts[symmetric])
   apply(simp_all only: Collect_neg_conj)
@@ -57,7 +57,7 @@
 
 lemma supp_fv:
   "supp t1 = fv_kind t1 \<and> supp t2 = fv_ty t2 \<and> supp t3 = fv_trm t3"
-  apply(induct rule: kind_ty_trm_induct)
+  apply(induct rule: kind_ty_trm.induct)
   apply(simp_all (no_asm) only: supp_eqs)
   apply(simp_all)
   apply(simp_all add: supp_eqs)