--- a/Nominal/Nominal2.thy	Fri Apr 20 15:29:40 2012 +0200
+++ b/Nominal/Nominal2.thy	Fri Apr 20 15:58:13 2012 +0200
@@ -332,12 +332,9 @@
 
   (* noting the quot_respects lemmas *)
   val (_, lthy6) = 
-    Local_Theory.note ((Binding.empty, [rsp_attr]),
-      raw_funs_rsp @ alpha_permute_rsp @ 
-      alpha_bn_rsp @ raw_perm_bn_rsp) lthy5
+    Local_Theory.note ((Binding.empty, [rsp_attr]), raw_funs_rsp) lthy5
 
-  val _ = tracing (PolyML.makestring (raw_size_rsp, raw_funs_rsp, alpha_permute_rsp,
-      alpha_bn_rsp, raw_perm_bn_rsp))
+  val _ = tracing (PolyML.makestring (raw_funs_rsp))
 
   val _ = trace_msg (K "Defining the quotient types...")
   val qty_descr = map (fn ((bind, vs, mx), _) => (map fst vs, bind, mx)) dts
@@ -372,21 +369,21 @@
     let
       val AlphaResult {alpha_bn_trms, ...} = alpha_result 
     in
-      map2 (fn (b, _, _) => fn t => ("alpha_" ^ Variable.check_name b, t, NoSyn, @{thm TrueI})) 
-        bn_funs  alpha_bn_trms
+      map2 (fn (b, _, _) => fn (t, th) => ("alpha_" ^ Variable.check_name b, t, NoSyn, th)) 
+        bn_funs (alpha_bn_trms ~~ alpha_bn_rsp)
     end
 
   val qperm_descr =
-    map2 (fn n => fn t => ("permute_" ^ n, Type.legacy_freeze t, NoSyn, @{thm TrueI})) 
-      qty_names raw_perm_funs
+    map2 (fn n => fn (t, th) => ("permute_" ^ n, Type.legacy_freeze t, NoSyn, th))
+      qty_names (raw_perm_funs ~~ (take (length raw_perm_funs) alpha_permute_rsp))
 
   val qsize_descr =
     map2 (fn n => fn (t, th) => ("size_" ^ n, t, NoSyn, th)) qty_names
       (raw_size_trms ~~ (take (length raw_size_trms) raw_size_rsp))
 
   val qperm_bn_descr = 
-    map2 (fn (b, _, _) => fn t => ("permute_" ^ Variable.check_name b, t, NoSyn, @{thm TrueI})) 
-      bn_funs raw_perm_bns
+    map2 (fn (b, _, _) => fn (t, th) => ("permute_" ^ Variable.check_name b, t, NoSyn, th))
+      bn_funs (raw_perm_bns ~~ raw_perm_bn_rsp)
 
   val ((((((qconstrs_infos, qbns_info), qfvs_info), qfv_bns_info), qalpha_bns_info), qperm_bns_info), 
     lthy8) =