diff -r b0e572776612 -r 24799397a3ce QuotMain.thy
--- a/QuotMain.thy	Wed Dec 02 10:30:20 2009 +0100
+++ b/QuotMain.thy	Wed Dec 02 10:56:35 2009 +0100
@@ -900,39 +900,42 @@
 lemma QUOT_TRUE_i: "(QUOT_TRUE (a :: bool) \<Longrightarrow> P) \<Longrightarrow> P"
 by (simp add: QUOT_TRUE_def)
 
-lemma QUOT_TRUE_imp: "QUOT_TRUE a"
+lemma QUOT_TRUE_imp: "QUOT_TRUE a \<equiv> QUOT_TRUE b"
 by (simp add: QUOT_TRUE_def)
 
 ML {*
-fun quot_true_tac ctxt fnctn =
-  CSUBGOAL (fn (cgl, i) =>
-  let
-    val gl = term_of cgl;
-    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_assums_hyp gl) of
-      SOME (_ $ (_ $ x)) =>
-        let
-          val thm' = Thm.lift_rule cgl @{thm QUOT_TRUE_imp}
-          val ps = Logic.strip_params (Thm.concl_of thm');
-          val fx = fnctn x;
-          val (_ $ (_ $ fx')) = Logic.strip_assums_concl (prop_of thm');
-            val insts = [(fx', fx)]
-            |> map (fn (t, u) => (cterm_of thy (Term.head_of t), cterm_of thy (Term.list_abs (ps, u))));
-          val thm_i = Drule.cterm_instantiate insts thm'
-          val thm_j = Thm.forall_elim_vars 1 thm_i
-        in
-          dtac thm_j i
-        end
-    | NONE => error "quot_true_tac!"
-    | _ => error "quot_true_tac!!"
-  end)
+fun quot_true_conv1 ctxt fnctn ctrm =
+  case (term_of ctrm) of
+    (Const (@{const_name QUOT_TRUE}, _) $ x) =>
+    let
+      val fx = fnctn x;
+      val thy = ProofContext.theory_of ctxt;
+      val cx = cterm_of thy x;
+      val cfx = cterm_of thy fx;
+      val cxt = ctyp_of thy (fastype_of x);
+      val cfxt = ctyp_of thy (fastype_of fx);
+      val thm = Drule.instantiate' [SOME cxt, SOME cfxt] [SOME cx, SOME cfx] @{thm QUOT_TRUE_imp}
+    in
+      Conv.rewr_conv thm ctrm
+    end
 *}
 
+ML {*
+fun quot_true_conv ctxt fnctn ctrm =
+  case (term_of ctrm) of
+    (Const (@{const_name QUOT_TRUE}, _) $ _) =>
+      quot_true_conv1 ctxt fnctn ctrm
+  | _ $ _ => Conv.comb_conv (quot_true_conv ctxt fnctn) ctrm
+  | Abs _ => Conv.abs_conv (fn (_, ctxt) => quot_true_conv ctxt fnctn) ctxt ctrm
+  | _ => Conv.all_conv ctrm
+*}
+
+ML {*
+fun quot_true_tac ctxt fnctn = CSUBGOAL (fn (goal, i) =>
+  CONVERSION
+    (Conv.params_conv ~1 (fn ctxt =>
+       (Conv.prems_conv ~1 (quot_true_conv ctxt fnctn))) ctxt) i)
+*}
 
 ML {* fun dest_comb (f $ a) = (f, a) *}
 ML {* fun dest_bcomb ((_ $ l) $ r) = (l, r) *}