--- a/QuotMain.thy	Tue Dec 01 16:27:42 2009 +0100
+++ b/QuotMain.thy	Tue Dec 01 18:22:48 2009 +0100
@@ -722,6 +722,7 @@
   ct |> term_of |> HOLogic.dest_Trueprop
 *}
 
+(* TODO: check if it still works with first_order_match *)
 ML {*
 fun instantiate_tac thm = 
   Subgoal.FOCUS (fn {concl, ...} =>
@@ -847,6 +848,38 @@
 apply(simp_all add: QUOT_TRUE_def)
 done
 
+lemma QUOT_TRUE_i: "(QUOT_TRUE a \<Longrightarrow> P) \<Longrightarrow> P"
+by (simp add: QUOT_TRUE_def)
+
+lemma QUOT_TRUE_imp: "QUOT_TRUE a \<Longrightarrow> QUOT_TRUE b"
+by (simp add: QUOT_TRUE_def)
+
+ML {*
+fun quot_true_tac ctxt fnctn =
+  SUBGOAL (fn (gl, _) =>
+  let
+    val thy = ProofContext.theory_of ctxt;
+    fun find_fun trm =
+      case trm of
+        (Const(@{const_name Trueprop}, _) $ (Const (@{const_name QUOT_TRUE}, _) $ _)) => true
+      | _ => false
+  in
+    case find_first find_fun (Logic.strip_imp_prems gl) of
+      SOME (_ $ (_ $ x)) =>
+        let
+          val fx = fnctn x;
+          val ctrm1 = cterm_of thy x;
+          val cty1 = ctyp_of thy (fastype_of x);
+          val ctrm2 = cterm_of thy fx;
+          val cty2 = ctyp_of thy (fastype_of fx);
+          val thm = Drule.instantiate' [SOME cty1, SOME cty2] [SOME ctrm1, SOME ctrm2] @{thm QUOT_TRUE_imp}
+        in
+          dtac thm 1
+        end
+    | NONE => error "quot_true_tac!"
+    | _ => error "quot_true_tac!!"
+  end)
+*}
 
 ML {*
 fun inj_repabs_tac ctxt rty quot_thms rel_refl trans2 =
@@ -1155,4 +1188,3 @@
 
 end
 
-