--- a/IntEx.thy	Sat Nov 21 14:18:31 2009 +0100
+++ b/IntEx.thy	Sat Nov 21 14:45:25 2009 +0100
@@ -249,21 +249,22 @@
 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}))]
+    [(K (print_tac "start")) THEN' (K no_tac), 
+     DT ctxt "1" (rtac trans_thm),
+     DT ctxt "2" (LAMBDA_RES_TAC ctxt),
+     DT ctxt "3" (ball_rsp_tac ctxt),
+     DT ctxt "4" (bex_rsp_tac ctxt),
+     DT ctxt "5" (FIRST' (map rtac rsp_thms)),
+     DT ctxt "6" (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' (RANGE [quotient_tac quot_thm])),
+     DT ctxt "7" (rtac refl),
+     DT ctxt "8" (APPLY_RSP_TAC rty ctxt THEN' (RANGE [quotient_tac quot_thm, quotient_tac quot_thm])),
+     DT ctxt "9" (Cong_Tac.cong_tac @{thm cong}),
+     DT ctxt "A" (rtac @{thm ext}),
+     DT ctxt "B" (rtac reflex_thm),
+     DT ctxt "C" (atac),
+     DT ctxt "D" (SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))),
+     DT ctxt "E" (WEAK_LAMBDA_RES_TAC ctxt),
+     DT ctxt "F" (CHANGED' (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ})))]
 *}
 
 ML {*
@@ -272,6 +273,13 @@
 val consts = lookup_quot_consts defs
 *}
 
+ML {* cprem_of *}
+
+ML {* 
+(mk_inj_REPABS_goal @{context} (reg_atrm, aqtrm) 
+  |> Syntax.check_term @{context})
+*}
+
 prove {* mk_inj_REPABS_goal @{context} (reg_atrm, aqtrm) *}
 apply(tactic {* ObjectLogic.full_atomize_tac 1 *})
 (* does not work *)