--- a/Quot/Nominal/LFex.thy	Wed Feb 24 15:39:17 2010 +0100
+++ b/Quot/Nominal/LFex.thy	Wed Feb 24 17:42:37 2010 +0100
@@ -20,6 +20,7 @@
 
 
 setup {* snd o define_raw_perms ["rkind", "rty", "rtrm"] ["LFex.rkind", "LFex.rty", "LFex.rtrm"] *}
+print_theorems
 
 local_setup {*
   snd o define_fv_alpha "LFex.rkind"
@@ -117,29 +118,11 @@
 thm rkind_rty_rtrm.inducts
 lemmas kind_ty_trm_inducts = rkind_rty_rtrm.inducts[quot_lifted]
 
-instantiation kind and ty and trm :: pt
-begin
-
-quotient_definition
-  "permute_kind :: perm \<Rightarrow> kind \<Rightarrow> kind"
-is
-  "permute :: perm \<Rightarrow> rkind \<Rightarrow> rkind"
-
-quotient_definition
-  "permute_ty :: perm \<Rightarrow> ty \<Rightarrow> ty"
-is
-  "permute :: perm \<Rightarrow> rty \<Rightarrow> rty"
-
-quotient_definition
-  "permute_trm :: perm \<Rightarrow> trm \<Rightarrow> trm"
-is
-  "permute :: perm \<Rightarrow> rtrm \<Rightarrow> rtrm"
-
-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
+setup {* define_lifted_perms ["LFex.kind", "LFex.ty", "LFex.trm"] 
+  [("permute_kind", @{term "permute :: perm \<Rightarrow> rkind \<Rightarrow> rkind"}),
+   ("permute_ty", @{term "permute :: perm \<Rightarrow> rty \<Rightarrow> rty"}),
+   ("permute_trm", @{term "permute :: perm \<Rightarrow> rtrm \<Rightarrow> rtrm"})]
+  @{thms permute_rkind_permute_rty_permute_rtrm_zero permute_rkind_permute_rty_permute_rtrm_append} *}
 
 (*
 Lifts, but slow and not needed?.