--- a/Nominal/Nominal2.thy	Thu Apr 12 01:39:54 2012 +0100
+++ b/Nominal/Nominal2.thy	Fri Apr 20 15:28:35 2012 +0200
@@ -321,7 +321,7 @@
       |> map mk_funs_rsp
 
   val raw_constrs_rsp = 
-    raw_constrs_rsp lthy5 alpha_result (flat raw_all_cns) (alpha_bn_imp_thms @ raw_funs_rsp_aux) 
+    raw_constrs_rsp lthy5 alpha_result raw_all_cns (alpha_bn_imp_thms @ raw_funs_rsp_aux) 
     
   val alpha_permute_rsp = map mk_alpha_permute_rsp alpha_eqvt
 
@@ -333,9 +333,12 @@
   (* noting the quot_respects lemmas *)
   val (_, lthy6) = 
     Local_Theory.note ((Binding.empty, [rsp_attr]),
-      raw_constrs_rsp @ raw_funs_rsp @ raw_size_rsp @ alpha_permute_rsp @ 
+      raw_funs_rsp @ alpha_permute_rsp @ 
       alpha_bn_rsp @ raw_perm_bn_rsp) lthy5
 
+  val _ = tracing (PolyML.makestring (raw_size_rsp, raw_funs_rsp, alpha_permute_rsp,
+      alpha_bn_rsp, raw_perm_bn_rsp))
+
   val _ = trace_msg (K "Defining the quotient types...")
   val qty_descr = map (fn ((bind, vs, mx), _) => (map fst vs, bind, mx)) dts
      
@@ -348,12 +351,12 @@
 
   val qtys = map #qtyp qty_infos
   val qty_full_names = map (fst o dest_Type) qtys
-  val qty_names = map Long_Name.base_name qty_full_names             
+  val qty_names = map Long_Name.base_name qty_full_names
 
   val _ = trace_msg (K "Defining the quotient constants...")
   val qconstrs_descrs =
-    (map2 o map2) (fn (b, _, mx) => fn t => (Variable.check_name b, t, mx, @{thm TrueI})) 
-      (get_cnstrs dts) raw_all_cns
+    (map2 o map2) (fn (b, _, mx) => fn (t, th) => (Variable.check_name b, t, mx, th))
+      (get_cnstrs dts) (map (op ~~) (raw_all_cns ~~ raw_constrs_rsp))
 
   val qbns_descr =
     map2 (fn (b, _, mx) => fn t => (Variable.check_name b, t, mx, @{thm TrueI})) bn_funs raw_bns
@@ -378,7 +381,8 @@
       qty_names raw_perm_funs
 
   val qsize_descr =
-    map2 (fn n => fn t => ("size_" ^ n, t, NoSyn, @{thm TrueI})) qty_names raw_size_trms
+    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}))