--- a/Nominal/Nominal2.thy	Mon Apr 30 15:45:23 2012 +0100
+++ b/Nominal/Nominal2.thy	Tue May 01 12:16:04 2012 +0100
@@ -53,7 +53,6 @@
 
 ML {*
 val eqvt_attr = Attrib.internal (K Nominal_ThmDecls.eqvt_add)
-val rsp_attr = Attrib.internal (K Quotient_Info.rsp_rules_add)
 val simp_attr = Attrib.internal (K Simplifier.simp_add)
 val induct_attr = Attrib.internal (K Induct.induct_simp_add)
 *}
@@ -313,15 +312,24 @@
   val _ = trace_msg (K "Proving respectfulness...")
   val raw_funs_rsp_aux = 
     raw_fv_bn_rsp_aux lthy5 alpha_result raw_fvs raw_bns raw_fv_bns (raw_bn_defs @ raw_fv_defs) 
-  
-  val raw_funs_rsp = map mk_funs_rsp raw_funs_rsp_aux
+
+  val raw_funs_rsp = map (Drule.eta_contraction_rule o mk_funs_rsp) raw_funs_rsp_aux
+
+  fun match_const cnst th =
+    (fst o dest_Const o snd o dest_comb o HOLogic.dest_Trueprop o prop_of) th =
+    fst (dest_Const cnst);
+  fun find_matching_rsp cnst =
+    hd (filter (fn th => match_const cnst th) raw_funs_rsp);
+  val raw_fv_rsp = map find_matching_rsp raw_fvs;
+  val raw_bn_rsp = map find_matching_rsp raw_bns;
+  val raw_fv_bn_rsp = map find_matching_rsp raw_fv_bns;
 
   val raw_size_rsp = 
     raw_size_rsp_aux lthy5 alpha_result (raw_size_thms @ raw_size_eqvt)
       |> 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
 
@@ -330,59 +338,54 @@
 
   val raw_perm_bn_rsp = raw_perm_bn_rsp lthy5 alpha_result raw_perm_bns raw_perm_bn_simps
 
-  (* 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 @ 
-      alpha_bn_rsp @ raw_perm_bn_rsp) lthy5
-
   val _ = trace_msg (K "Defining the quotient types...")
   val qty_descr = map (fn ((bind, vs, mx), _) => (map fst vs, bind, mx)) dts
-     
-  val (qty_infos, lthy7) = 
+
+  val (qty_infos, lthy7) =
     let
       val AlphaResult {alpha_trms, alpha_tys, ...} = alpha_result
     in
-      define_qtypes qty_descr alpha_tys alpha_trms alpha_equivp_thms lthy6
+      define_qtypes qty_descr alpha_tys alpha_trms alpha_equivp_thms lthy5
     end
 
   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
+    map2 (fn (b, _, mx) => fn (t, th) => (Variable.check_name b, t, mx, th)) bn_funs (raw_bns ~~ raw_bn_rsp)
 
-  val qfvs_descr = 
-    map2 (fn n => fn t => ("fv_" ^ n, t, NoSyn, @{thm TrueI})) qty_names raw_fvs
+  val qfvs_descr =
+    map2 (fn n => fn (t, th) => ("fv_" ^ n, t, NoSyn, th)) qty_names (raw_fvs ~~ raw_fv_rsp)
 
-  val qfv_bns_descr = 
-    map2 (fn (b, _, _) => fn t => ("fv_" ^ Variable.check_name b, t, NoSyn, @{thm TrueI})) 
-      bn_funs raw_fv_bns
+  val qfv_bns_descr =
+    map2 (fn (b, _, _) => fn (t, th) => ("fv_" ^ Variable.check_name b, t, NoSyn, th))
+      bn_funs (raw_fv_bns ~~ raw_fv_bn_rsp)
 
   val qalpha_bns_descr = 
     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 => ("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})) 
-      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) =