--- a/QuotMain.thy	Fri Dec 04 11:33:58 2009 +0100
+++ b/QuotMain.thy	Fri Dec 04 12:20:49 2009 +0100
@@ -708,7 +708,6 @@
 
 section {* RepAbs Injection Tactic *}
 
-(* TODO: check if it still works with first_order_match *)
 (* FIXME/TODO: do not handle everything *)
 ML {*
 fun instantiate_tac thm = 
@@ -1026,6 +1025,31 @@
   REPEAT_ALL_NEW (inj_repabs_tac ctxt rel_refl trans2)
 *}
 
+ML {*
+fun dest_fun_type (Type("fun", [T, S])) = (T, S)
+  | dest_fun_type _ = error "dest_fun_type"
+*}
+
+ML {*
+val rep_abs_rsp_tac =
+  Subgoal.FOCUS (fn {concl, context, ...} =>
+    case HOLogic.dest_Trueprop (term_of concl) of (rel $ lhs $ (rep $ (abs $ rhs))) =>
+    (let
+      val thy = ProofContext.theory_of context;
+      val (ty_a, ty_b) = dest_fun_type (fastype_of abs);
+      val ty_inst = map (SOME o (ctyp_of thy)) [ty_a, ty_b];
+      val t_inst = map (SOME o (cterm_of thy)) [rel, abs, rep];
+      val thm = Drule.instantiate' ty_inst t_inst @{thm REP_ABS_RSP}
+      val te = solve_quotient_assums context thm
+      val t_inst = map (SOME o (cterm_of thy)) [lhs, rhs];
+      val thm = Drule.instantiate' [] t_inst te
+    in
+      compose_tac (false, thm, 1) 1
+    end
+    handle _ => no_tac)
+  | _ => no_tac)
+*}
+
 (* A faster version *)
 
 ML {*
@@ -1054,7 +1078,8 @@
     (resolve_tac trans2 THEN' RANGE [
       quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)])
 | _ $ _ $ _ =>
-    instantiate_tac @{thm REP_ABS_RSP} ctxt THEN' RANGE [SOLVES' (quotient_tac ctxt)]
+    rep_abs_rsp_tac ctxt
+| _ => error "inj_repabs_tac not a relation"
 ) i)
 *}
 
@@ -1108,12 +1133,6 @@
 *}
 
 ML {*
-fun dest_fun_type (Type("fun", [T, S])) = (T, S)
-  | dest_fun_type _ = error "dest_fun_type"
-*}
-
-
-ML {*
 fun lambda_allex_prs_simple_conv ctxt ctrm =
   case (term_of ctrm) of
     ((Const (@{const_name fun_map}, _) $ r1 $ a2) $ (Abs _)) =>