--- a/Nominal/Nominal2.thy	Fri Apr 20 15:58:13 2012 +0200
+++ b/Nominal/Nominal2.thy	Fri Apr 20 18:58:03 2012 +0200
@@ -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,8 +312,17 @@
   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)
@@ -330,20 +338,14 @@
 
   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_funs_rsp) lthy5
-
-  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
-     
-  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
@@ -356,14 +358,14 @@
       (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