--- 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" } *}