--- a/QuotMain.thy	Wed Dec 02 10:56:35 2009 +0100
+++ b/QuotMain.thy	Wed Dec 02 11:30:40 2009 +0100
@@ -840,21 +840,36 @@
 
 *}
 
-
-
+definition
+  "QUOT_TRUE x \<equiv> True"
 
 ML {*
-fun APPLY_RSP_TAC rty = 
-  Subgoal.FOCUS (fn {concl, ...} =>
-    case HOLogic.dest_Trueprop (term_of concl) of
-       (_ $ (f $ _) $ (_ $ _)) =>
+fun find_qt_asm asms =
+  let
+    fun find_fun trm =
+      case trm of
+        (Const(@{const_name Trueprop}, _) $ (Const (@{const_name QUOT_TRUE}, _) $ _)) => true
+      | _ => false
+  in
+    case find_first find_fun asms of
+      SOME (_ $ (_ $ (f $ a))) => (f, a)
+    | _ => error "find_qt_asm"
+  end
+*}
+
+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.match (pat, concl)
           in
-            if needs_lift rty (fastype_of f) 
-            then rtac (Drule.instantiate insts @{thm APPLY_RSP}) 1
-            else no_tac
+            if (fastype_of asmf) = (fastype_of f)
+            then no_tac
+            else rtac (Drule.instantiate insts @{thm APPLY_RSP}) 1
           end
      | _ => no_tac)
 *}
@@ -886,9 +901,6 @@
 
 *)
 
-definition 
-  "QUOT_TRUE x \<equiv> True"
-
 lemma quot_true_dests:
   shows QT_all: "QUOT_TRUE (All P) \<Longrightarrow> QUOT_TRUE P"
   and   QT_ex:  "QUOT_TRUE (Ex P) \<Longrightarrow> QUOT_TRUE P"
@@ -942,7 +954,7 @@
 ML {* fun unlam (Abs a) = snd (Term.dest_abs a) *}
 
 ML {*
-fun inj_repabs_tac ctxt rty quot_thms rel_refl trans2 =
+fun inj_repabs_tac_old ctxt rty quot_thms rel_refl trans2 =
   (FIRST' [
     (* "cong" rule of the of the relation / transitivity*)
     (* (op =) (R a b) (R c d) ----> \<lbrakk>R a c; R b d\<rbrakk> *)
@@ -998,11 +1010,11 @@
 *}
 
 ML {*
-fun inj_repabs_tac' ctxt rty quot_thms rel_refl trans2 =
+fun inj_repabs_tac ctxt rty quot_thms rel_refl trans2 =
   (FIRST' [
     (* "cong" rule of the of the relation / transitivity*)
     (* (op =) (R a b) (R c d) ----> \<lbrakk>R a c; R b d\<rbrakk> *)
-    DT ctxt "1" (resolve_tac trans2),
+    NDT ctxt "1" (resolve_tac trans2),
 
     (* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>y\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *)
     NDT ctxt "2" (lambda_rsp_tac THEN' quot_true_tac ctxt unlam),