diff -r 7926f1cb45eb -r e8ec504dddf2 Nominal/Nominal2.thy
--- 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 *)