--- a/Nominal/Ex/Foo1.thy	Sat Nov 13 10:25:03 2010 +0000
+++ b/Nominal/Ex/Foo1.thy	Sat Nov 13 22:23:26 2010 +0000
@@ -42,20 +42,6 @@
 thm foo.supp
 thm foo.fresh
 
-quotient_definition
-  "permute_bn1 :: perm \<Rightarrow> assg \<Rightarrow> assg"
-is
-  "permute_bn1_raw"
-
-quotient_definition
-  "permute_bn2 :: perm \<Rightarrow> assg \<Rightarrow> assg"
-is
-  "permute_bn2_raw"
-
-quotient_definition
-  "permute_bn3 :: perm \<Rightarrow> assg \<Rightarrow> assg"
-is
-  "permute_bn3_raw"
 
 lemmas permute_bn1 = permute_bn1_raw.simps[quot_lifted]
 lemmas permute_bn2 = permute_bn2_raw.simps[quot_lifted]

--- a/Nominal/Ex/Let.thy	Sat Nov 13 10:25:03 2010 +0000
+++ b/Nominal/Ex/Let.thy	Sat Nov 13 22:23:26 2010 +0000
@@ -18,8 +18,6 @@
   "bn ANil = []"
 | "bn (ACons x t as) = (atom x) # (bn as)"
 
-thm permute_bn_raw.simps
-
 thm at_set_avoiding2
 thm trm_assn.fv_defs
 thm trm_assn.eq_iff 
@@ -32,11 +30,6 @@
 thm trm_assn.fresh
 thm trm_assn.exhaust[where y="t", no_vars]
 
-quotient_definition
-  "permute_bn :: perm \<Rightarrow> assn \<Rightarrow> assn"
-is
-  "permute_bn_raw"
-
 lemmas permute_bn = permute_bn_raw.simps[quot_lifted]
 
 lemma uu:

--- a/Nominal/Ex/SingleLet.thy	Sat Nov 13 10:25:03 2010 +0000
+++ b/Nominal/Ex/SingleLet.thy	Sat Nov 13 22:23:26 2010 +0000
@@ -36,22 +36,6 @@
 thm single_let.supp
 thm single_let.fresh
 
-quotient_definition
-  "permute_bn :: perm \<Rightarrow> assg \<Rightarrow> assg"
-is
-  "permute_bn_raw"
-
-lemma [quot_respect]:
-  shows "((op =) ===> alpha_assg_raw ===> alpha_assg_raw) permute_bn_raw permute_bn_raw"
-  apply (simp add: fun_rel_def)
-  apply clarify
-  apply (erule alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.inducts)
-  apply (rule TrueI)+
-  apply simp_all
-  apply (rule_tac [!] alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros)
-  apply simp_all
-  done
-
 lemmas permute_bn = permute_bn_raw.simps[quot_lifted]
 
 lemma uu:

--- a/Nominal/Nominal2.thy	Sat Nov 13 10:25:03 2010 +0000
+++ b/Nominal/Nominal2.thy	Sat Nov 13 22:23:26 2010 +0000
@@ -498,7 +498,11 @@
   val qsize_descr =
     map2 (fn n => fn t => ("size_" ^ n, t, NoSyn)) qty_names raw_size_trms
 
-  val (((((qconstrs_info, qbns_info), qfvs_info), qfv_bns_info), qalpha_bns_info), lthy8) = 
+  val qperm_bn_descr = 
+    map2 (fn (b, _, _) => fn t => ("permute_" ^ Name.of_binding b, t, NoSyn)) bn_funs raw_perm_bns
+     
+
+  val ((((((qconstrs_info, qbns_info), qfvs_info), qfv_bns_info), qalpha_bns_info), qpermute_bns), lthy8) = 
     if get_STEPS lthy > 24
     then 
       lthy7
@@ -507,6 +511,7 @@
       ||>> define_qconsts qtys qfvs_descr
       ||>> define_qconsts qtys qfv_bns_descr
       ||>> define_qconsts qtys qalpha_bns_descr
+      ||>> define_qconsts qtys qperm_bn_descr
     else raise TEST lthy7
 
   (* definition of the quotient permfunctions and pt-class *)