--- a/QuotMain.thy	Thu Dec 03 11:34:34 2009 +0100
+++ b/QuotMain.thy	Thu Dec 03 11:58:46 2009 +0100
@@ -715,7 +715,6 @@
 
 section {* RepAbs Injection Tactic *}
 
-(* TODO: check if it still works with first_order_match *)
 ML {*
 fun instantiate_tac thm = 
   Subgoal.FOCUS (fn {concl, ...} =>
@@ -771,14 +770,6 @@
       | _ => no_tac)
 *}
 
-ML {* (* Legacy *)
-fun needs_lift (rty as Type (rty_s, _)) ty =
-  case ty of
-    Type (s, tys) => (s = rty_s) orelse (exists (needs_lift rty) tys)
-  | _ => false
-
-*}
-
 definition
   "QUOT_TRUE x \<equiv> True"
 
@@ -797,24 +788,7 @@
 *}
 
 ML {*
-fun APPLY_RSP_TAC rty =
-  Subgoal.FOCUS (fn {concl, asms, ...} =>
-    case ((HOLogic.dest_Trueprop (term_of concl))) of
-       ((_ $ (f $ _) $ (_ $ _))) =>
-          let
-            val (asmf, asma) = find_qt_asm (map term_of asms);
-            val pat = Drule.strip_imp_concl (cprop_of @{thm APPLY_RSP});
-            val insts = Thm.first_order_match (pat, concl)
-          in
-            if (fastype_of asmf) = (fastype_of f)
-            then no_tac
-            else rtac (Drule.instantiate insts @{thm APPLY_RSP}) 1
-          end
-     | _ => no_tac)
-*}
-
-ML {*
-val APPLY_RSP_TAC' =
+val APPLY_RSP_TAC =
   Subgoal.FOCUS (fn {concl, asms, context,...} =>
     case ((HOLogic.dest_Trueprop (term_of concl))) of
        ((R2 $ (f $ x) $ (g $ y))) =>
@@ -960,7 +934,7 @@
                   THEN' (RANGE [SOLVES' (quotient_tac ctxt quot_thms)]))),
 
     (* R (t $ \<dots>) (t' $ \<dots>) ----> APPLY_RSP   provided type of t needs lifting *)
-    NDT ctxt "A" (APPLY_RSP_TAC' ctxt THEN'
+    NDT ctxt "A" (APPLY_RSP_TAC ctxt THEN'
                 (RANGE [SOLVES' (quotient_tac ctxt quot_thms), SOLVES' (quotient_tac ctxt quot_thms),
                         quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)])),