diff -r bb23a7393de3 -r 6cdba30c6d66 QuotMain.thy
--- a/QuotMain.thy	Thu Dec 03 14:00:43 2009 +0100
+++ b/QuotMain.thy	Thu Dec 03 14:02:05 2009 +0100
@@ -790,24 +790,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))) =>
@@ -953,7 +936,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)])),
 
@@ -1107,8 +1090,10 @@
 *)
 
 ML {*
-fun clean_tac lthy quot defs =
+fun clean_tac lthy quot =
   let
+    val thy = ProofContext.theory_of lthy;
+    val defs = map (Thm.varifyT o #def) (qconsts_dest thy);
     val absrep = map (fn x => @{thm QUOTIENT_ABS_REP} OF [x]) quot
     val meta_absrep = map (fn x => @{thm eq_reflection} OF [x]) absrep;
     val reps_same = map (fn x => @{thm QUOTIENT_REL_REP} OF [x]) quot
@@ -1232,7 +1217,7 @@
 ML {*
 (* FIXME/TODO should only get as arguments the rthm like procedure_tac *)
 
-fun lift_tac lthy rthm rel_eqv quot defs =
+fun lift_tac lthy rthm rel_eqv quot =
   ObjectLogic.full_atomize_tac
   THEN' gen_frees_tac lthy
   THEN' Subgoal.FOCUS (fn {context, concl, ...} =>
@@ -1248,7 +1233,7 @@
         RANGE [rtac rthm',
                regularize_tac lthy rel_eqv,
                rtac thm THEN' all_inj_repabs_tac lthy quot rel_refl trans2,
-               clean_tac lthy quot defs]]
+               clean_tac lthy quot]]
     end) lthy
 *}