diff -r ea6a52a4f5bf -r d1ab27c10049 Quot/Nominal/LFex.thy
--- a/Quot/Nominal/LFex.thy	Wed Feb 24 15:36:07 2010 +0100
+++ b/Quot/Nominal/LFex.thy	Wed Feb 24 15:39:17 2010 +0100
@@ -135,25 +135,9 @@
 is
   "permute :: perm \<Rightarrow> rtrm \<Rightarrow> rtrm"
 
-lemmas permute_ktt[simp] = permute_rkind_permute_rty_permute_rtrm.simps[quot_lifted]
-
-lemma perm_zero_ok: "0 \<bullet> (x :: kind) = x \<and> 0 \<bullet> (y :: ty) = y \<and> 0 \<bullet> (z :: trm) = z"
-apply (induct rule: kind_ty_trm_induct)
-apply (simp_all)
-done
-
-lemma perm_add_ok:
-  "((p + q) \<bullet> (x1 :: kind) = (p \<bullet> q \<bullet> x1))"
-  "((p + q) \<bullet> (x2 :: ty) = p \<bullet> q \<bullet> x2)"
-  "((p + q) \<bullet> (x3 :: trm) = p \<bullet> q \<bullet> x3)"
-apply (induct x1 and x2 and x3 rule: kind_ty_trm_inducts)
-apply (simp_all)
-done
-
-instance
-apply default
-apply (simp_all add: perm_zero_ok perm_add_ok)
-done
+instance by default (simp_all add:
+  permute_rkind_permute_rty_permute_rtrm_zero[quot_lifted]
+  permute_rkind_permute_rty_permute_rtrm_append[quot_lifted])
 
 end
 
@@ -162,6 +146,8 @@
 lemmas alpha_kind_alpha_ty_alpha_trm_induct = alpha_rkind_alpha_rty_alpha_rtrm.induct[unfolded alpha_gen, quot_lifted, folded alpha_gen]
 *)
 
+lemmas permute_ktt[simp] = permute_rkind_permute_rty_permute_rtrm.simps[quot_lifted]
+
 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]