--- a/IntEx.thy	Sat Nov 21 13:14:35 2009 +0100
+++ b/IntEx.thy	Sat Nov 21 14:18:31 2009 +0100
@@ -175,7 +175,7 @@
 *}
 
 ML {*
-fun inj_REPABS_aux lthy (rtrm, qtrm) =
+fun inj_REPABS lthy (rtrm, qtrm) =
 let
   val rty = fastype_of rtrm
   val qty = fastype_of qtrm
@@ -186,7 +186,7 @@
       val (y, s) = Term.dest_abs (x, T, t)
       val (y', s') = Term.dest_abs (x', T', t')
       val yvar = Free (y, T)
-      val res = lambda yvar (inj_REPABS_aux lthy (s, s'))
+      val res = lambda yvar (inj_REPABS lthy (s, s'))
     in
       if T = T'
       then res
@@ -194,15 +194,15 @@
     end
   (* FIXME: Does one havae to look at the abstraction or go under the lambda. *) 
   | (Const (@{const_name "Ball"}, T) $ r $ t, Const (@{const_name "All"}, _) $ t') =>
-      Const (@{const_name "Ball"}, T) $ r $ (inj_REPABS_aux lthy (t, t'))
+      Const (@{const_name "Ball"}, T) $ r $ (inj_REPABS lthy (t, t'))
   | (Const (@{const_name "Bex"}, T) $ r $ t, Const (@{const_name "Ex"}, _) $ t') =>
-      Const (@{const_name "Bex"}, T) $ r $ (inj_REPABS_aux lthy (t, t'))
+      Const (@{const_name "Bex"}, T) $ r $ (inj_REPABS lthy (t, t'))
   | (rtrm as _ $ _, qtrm as _ $ _) => 
     let
       val (rhead, rargs) = Term.strip_comb rtrm
       val (qhead, qargs) = Term.strip_comb qtrm
-      val rhead' = inj_REPABS_aux lthy (rhead, qhead)
-      val rargs' = map (inj_REPABS_aux lthy) (rargs ~~ qargs)
+      val rhead' = inj_REPABS lthy (rhead, qhead)
+      val rargs' = map (inj_REPABS lthy) (rargs ~~ qargs)
       val res = list_comb (rhead', rargs')
     in
       if rty = qty
@@ -214,11 +214,9 @@
 end
 *}
 
-
 ML {*
-fun inj_REPABS lthy (rtrm, qtrm) =
-  inj_REPABS_aux lthy (rtrm, qtrm)
-  |> Syntax.check_term lthy
+fun mk_inj_REPABS_goal lthy (rtrm, qtrm) =
+  Logic.mk_equals (rtrm, Syntax.check_term lthy (inj_REPABS lthy (rtrm, qtrm)))
 *}
 
 lemma plus_assoc_pre:
@@ -246,11 +244,41 @@
 
 ML {* @{thm testtest} OF [arthm] *}
 
-ML {* 
-  val reg_atrm = prop_of (@{thm testtest} OF [arthm]);
+ML {* val reg_atrm = prop_of (@{thm testtest} OF [arthm]) *}
+
+ML {*
+fun r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms =
+  (REPEAT1 o FIRST1) 
+    [rtac trans_thm,
+     LAMBDA_RES_TAC ctxt,
+     ball_rsp_tac ctxt,
+     bex_rsp_tac ctxt,
+     FIRST' (map rtac rsp_thms),
+     (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' (RANGE [quotient_tac quot_thm])),
+     rtac refl,
+     (APPLY_RSP_TAC rty ctxt THEN' (RANGE [quotient_tac quot_thm, quotient_tac quot_thm])),
+     Cong_Tac.cong_tac @{thm cong},
+     rtac @{thm ext},
+     rtac reflex_thm,
+     atac,
+     SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps})),
+     WEAK_LAMBDA_RES_TAC ctxt,
+     CHANGED' (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ}))]
 *}
 
 ML {*
+val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} @{typ "my_int"}
+val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "my_int"
+val consts = lookup_quot_consts defs
+*}
+
+prove {* mk_inj_REPABS_goal @{context} (reg_atrm, aqtrm) *}
+apply(tactic {* ObjectLogic.full_atomize_tac 1 *})
+(* does not work *)
+apply(tactic {* r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms *})
+
+
+ML {*
 inj_REPABS @{context} (reg_atrm, aqtrm)  
 |> Syntax.string_of_term @{context}
 |> writeln