--- a/QuotMain.thy	Mon Dec 07 12:14:25 2009 +0100
+++ b/QuotMain.thy	Mon Dec 07 14:00:36 2009 +0100
@@ -907,6 +907,11 @@
     (Const(@{const_name Bex},_) $ (Const (@{const_name Respects}, _) $ _) $ _)
       => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam
 
+| (_ $
+    (Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _) $
+    (Const(@{const_name Babs},_) $ (Const (@{const_name Respects}, _) $ _) $ _))
+      => rtac @{thm babs_rsp} THEN' RANGE [quotient_tac ctxt]
+
     (* reflexivity of operators arising from Cong_tac *)
 | Const (@{const_name "op ="},_) $ _ $ _ 
       => rtac @{thm refl} ORELSE'
@@ -993,6 +998,7 @@
        val lpi = Drule.instantiate' tyinst tinst @{thm lambda_prs}
        val te = @{thm eq_reflection} OF [solve_quotient_assums ctxt (solve_quotient_assums ctxt lpi)]
        val ts = MetaSimplifier.rewrite_rule @{thms id_simps} te
+       val _ = tracing ("te rule:\n" ^ (Syntax.string_of_term ctxt (prop_of te)));
        val tl = Thm.lhs_of ts
        val (insp, inst) = make_inst (term_of tl) (term_of ctrm)
        val ti = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts