--- a/IntEx.thy	Mon Nov 23 13:46:14 2009 +0100
+++ b/IntEx.thy	Mon Nov 23 13:55:31 2009 +0100
@@ -161,75 +161,6 @@
 apply(tactic {* REGULARIZE_tac' @{context} @{thm "TrueI"} @{thm my_int_equiv} *})
 done
 
-(* rep-abs injection *)
-
-ML {*
-(* FIXME: is this the right get_fun function for rep-abs injection *)
-fun mk_repabs lthy (T, T') trm = 
-  Quotient_Def.get_fun repF lthy (T, T') 
-  $ (Quotient_Def.get_fun absF lthy (T, T') $ trm)
-*}
-
-ML {*
-(* replaces a term for the bound variable, *)
-(* possible capture                        *)
-fun replace_bnd0 (trm, Abs (x, T, t)) =
-  Abs (x, T, subst_bound (trm, t))
-*}
-
-
-ML {*
-(* bound variables need to be treated properly,  *)
-(* as the type of subterms need to be calculated *)
-
-fun is_lifted_const h gh = is_Const h andalso is_Const gh andalso not (h = gh)
-
-fun inj_REPABS lthy (rtrm, qtrm) =
-let
-  val rty = fastype_of rtrm
-  val qty = fastype_of qtrm
-in
-  case (rtrm, qtrm) of
-    (Const (@{const_name "Ball"}, T) $ r $ t, Const (@{const_name "All"}, _) $ 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 lthy (t, t'))
-  | (Const (@{const_name "Babs"}, T) $ r $ t, t') =>
-       Const (@{const_name "Babs"}, T) $ r $ (inj_REPABS lthy (t, t'))
-  | (Abs (x, T, t), Abs (x', T', t')) =>
-      let
-        val (y, s) = Term.dest_abs (x, T, t)
-        val (_, s') = Term.dest_abs (x', T', t')
-        val yvar = Free (y, T)
-        val res = lambda yvar (inj_REPABS lthy (s, s'))
-      in
-        if rty = qty
-        then res
-        else if T = T'
-             then mk_repabs lthy (rty, qty) res
-             else mk_repabs lthy (rty, qty) (replace_bnd0 (mk_repabs lthy (T, T') (Bound 0), res))
-      end
-  | _ =>
-      let
-        val (rhead, rargs) = strip_comb rtrm
-        val (qhead, qargs) = strip_comb qtrm
-        (* TODO:  val rhead' = inj_REPABS lthy (rhead, qhead) *)
-        val rhead' = rhead;
-        val rargs' = map (inj_REPABS lthy) (rargs ~~ qargs);
-        val result = list_comb (rhead', rargs');
-      in
-        if rty = qty then result else
-        if (is_lifted_const rhead qhead) then mk_repabs lthy (rty, qty) result else
-        if ((Term.is_Free rhead) andalso (length rargs' > 0)) then mk_repabs lthy (rty, qty) result else
-        if rargs' = [] then rhead' else result
-      end
-end
-*}
-
-ML {*
-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:
   shows "my_plus (my_plus i j) k \<approx> my_plus i (my_plus j k)"
@@ -244,7 +175,6 @@
 ML {*
   val arthm = atomize_thm @{thm plus_assoc_pre}
   val aqthm = atomize_thm test2
-
   val aqtrm = prop_of aqthm
   val artrm = prop_of arthm
 *}
@@ -258,6 +188,8 @@
 
 ML {* val reg_atrm = prop_of (@{thm testtest} OF [arthm]) *}
 
+(*
+does not work.
 ML {*
 fun r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms =
   (REPEAT1 o FIRST1) 
@@ -278,6 +210,7 @@
      DT ctxt "E" (WEAK_LAMBDA_RES_TAC ctxt),
      DT ctxt "F" (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"}
@@ -298,9 +231,8 @@
 
 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 *})
-
+apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms) 1 *})
+done
 
 ML {*
 inj_REPABS @{context} (reg_atrm, aqtrm)