--- a/QuotMain.thy	Thu Sep 17 12:06:06 2009 +0200
+++ b/QuotMain.thy	Thu Sep 17 16:55:11 2009 +0200
@@ -822,32 +822,76 @@
       if bop_s = "op =" then pair else (raise CTERM ("Not an equality", [t]))
     end
 *}
+ML Thm.instantiate
+ML {*@{thm arg_cong2}*}
+ML {*@{thm arg_cong2[of _ _ _ _ "op ="]} *}
+ML {* val cT = @{cpat "op ="} |> Thm.ctyp_of_term |> Thm.dest_ctyp |> hd *}
+ML {* 
+  Toplevel.program (fn () =>
+    Drule.instantiate' [SOME cT,SOME cT,SOME @{ctyp bool}] [NONE,NONE,NONE,NONE,SOME (@{cpat "op ="})] @{thm arg_cong2}
+  )
+*}
+
 ML {*
-  fun foo_conv ctxt t =
+  fun foo_conv t =
     let
       val (lhs, rhs) = dest_ceq t;
       val (bop, _) = dest_cbinop lhs;
-(*      val _ = tracing (Syntax.string_of_term ctxt (Thm.term_of lhs))*)
+      val [clT, cr2] = bop |> Thm.ctyp_of_term |> Thm.dest_ctyp;
+      val [cmT, crT] = Thm.dest_ctyp cr2;
     in
-      @{thm arg_cong2}
+      Drule.instantiate' [SOME clT,SOME cmT,SOME crT] [NONE,NONE,NONE,NONE,SOME bop] @{thm arg_cong2}
     end
 *}
+
+ML ORELSE
+
 ML {*
-  fun foo_tac ctxt thm =
+  fun foo_tac n thm =
     let
-      val concl = Thm.concl_of thm;
-      val (_, cconcl) = Thm.dest_comb (Thm.cterm_of @{theory} concl);
-      val (_, cconcl) = Thm.dest_comb cconcl;
-      val rewr = foo_conv ctxt cconcl;
-      val _ = tracing (Syntax.string_of_term ctxt (Thm.term_of cconcl))
+      val concl = Thm.cprem_of thm n;
+      val (_, cconcl) = Thm.dest_comb concl;
+      val rewr = foo_conv cconcl;
+      val _ = tracing (Display.string_of_thm @{context} rewr)
+      val _ = tracing (Display.string_of_thm @{context} thm)
     in
-      Seq.single thm
+      rtac rewr n thm
     end
+      handle CTERM _ => Seq.empty
 *}
+
+ML foo_tac
+ML {*
+  val foo_tac' =
+    FIRST' [
+      rtac @{thm list_eq_sym},
+      rtac @{thm cons_preserves},
+      rtac @{thm mem_respects},
+      foo_tac,
+      simp_tac (@{simpset} addsimps @{thms QUOT_TYPE_I_fset.REP_ABS_rsp})
+    ]
+*}
+
 ML {* Thm.assume @{cprop "0 = 0"} *}
 
+ML simp_tac
+
 prove {* HOLogic.mk_Trueprop (Thm.term_of cgoal2) *}
-apply (tactic {* foo_tac @{context} *})
+apply (tactic {* foo_tac' 1 *})
+unfolding IN_def INSERT_def
+apply (tactic {* foo_tac' 1 *})
+apply (tactic {* foo_tac' 1 *})
+apply (tactic {* foo_tac' 1 *})
+apply (tactic {* foo_tac' 1 *})
+apply (tactic {* foo_tac' 1 *})
+apply (tactic {* foo_tac' 1 *})
+apply (tactic {* foo_tac' 1 *})
+apply (tactic {* foo_tac' 1 *})
+apply (tactic {* foo_tac' 1 *})
+apply (tactic {* foo_tac' 1 *})
+apply (tactic {* foo_tac' 1 *})
+apply (tactic {* foo_tac' 1 *})
+done
 
 (*
 datatype obj1 =