--- a/QuotMain.thy	Fri Oct 16 16:51:01 2009 +0200
+++ b/QuotMain.thy	Fri Oct 16 17:05:52 2009 +0200
@@ -1192,6 +1192,7 @@
 
 prove trm
 apply (atomize(full))
+apply (simp only: id_def[symmetric])
 
 ML_prf {*
   val gc = Subgoal.focus @{context} 1 (Isar.goal ())
@@ -1215,6 +1216,20 @@
   val (_, tc') = Thm.dest_comb tc
   val (_, gc') = Thm.dest_comb gc
  *}
+ML_prf {*
+  fun dest_cbinop t =
+    let
+      val (t2, rhs) = Thm.dest_comb t;
+      val (bop, lhs) = Thm.dest_comb t2;
+    in
+      (bop, (lhs, rhs))
+    end
+*}
+
+ML_prf {* val (op1, (l1, r1)) = dest_cbinop tc' *}
+ML_prf {* val (op2, (l2, r2)) = dest_cbinop gc' *}
+ML_prf {* val mr = Thm.match (r1, r2) *}
+
 
 ML_prf {* val m = Thm.match (tc', gc') *}
 ML_prf {* val t2 = Drule.instantiate m @{thm "REP_ABS_RSP_I" } *}

--- a/QuotScript.thy	Fri Oct 16 16:51:01 2009 +0200
+++ b/QuotScript.thy	Fri Oct 16 17:05:52 2009 +0200
@@ -307,8 +307,14 @@
   assumes q: "QUOTIENT R Abs Rep"
   and     a: "R x1 x2"
   shows "R x1 (Rep (Abs x2))"
-using a
-by (metis QUOTIENT_REL[OF q] QUOTIENT_ABS_REP[OF q] QUOTIENT_REP_REFL[OF q])
+  and   "R (Rep (Abs x1)) x2"
+proof -
+  show "R x1 (Rep (Abs x2))" 
+    using q a by (metis QUOTIENT_REL[OF q] QUOTIENT_ABS_REP[OF q] QUOTIENT_REP_REFL[OF q])
+next
+  show "R (Rep (Abs x1)) x2"
+    using q a by (metis QUOTIENT_REL[OF q] QUOTIENT_ABS_REP[OF q] QUOTIENT_REP_REFL[OF q] QUOTIENT_SYM[of q])
+qed
 
 (* ----------------------------------------------------- *)
 (* Quantifiers: FORALL, EXISTS, EXISTS_UNIQUE,           *)