diff -r d1ab27c10049 -r cff8a67691d2 Quot/Nominal/Terms.thy
--- a/Quot/Nominal/Terms.thy	Wed Feb 24 15:39:17 2010 +0100
+++ b/Quot/Nominal/Terms.thy	Wed Feb 24 17:42:37 2010 +0100
@@ -150,18 +150,8 @@
 lemmas trm1_bp_induct = rtrm1_bp.induct[quot_lifted]
 lemmas trm1_bp_inducts = rtrm1_bp.inducts[quot_lifted]
 
-instantiation trm1 and bp :: pt
-begin
-
-quotient_definition
-  "permute_trm1 :: perm \<Rightarrow> trm1 \<Rightarrow> trm1"
-is
-  "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1"
-
-instance by default 
-  (simp_all add: permute_rtrm1_permute_bp_zero[quot_lifted] permute_rtrm1_permute_bp_append[quot_lifted])
-
-end
+setup {* define_lifted_perms ["Terms.trm1"] [("permute_trm1", @{term "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1"})]
+  @{thms permute_rtrm1_permute_bp_zero permute_rtrm1_permute_bp_append} *}
 
 lemmas
     permute_trm1 = permute_rtrm1_permute_bp.simps[quot_lifted]