# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1259415922 -3600
# Node ID 84ee3973f0830c6c2fd8415f6111261a12373712
# Parent  f1c0a66284d314d803d9deeeb9804517d51e0eb2
removed old inj_repabs_tac; kept only the one with (selective) debugging information

diff -r f1c0a66284d3 -r 84ee3973f083 FSet.thy
--- a/FSet.thy	Sat Nov 28 14:33:04 2009 +0100
+++ b/FSet.thy	Sat Nov 28 14:45:22 2009 +0100
@@ -328,7 +328,7 @@
 apply (tactic {* lift_tac_fset @{context} @{thm not_mem_card1} 1 *})
 done
 
-ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac' lthy rty [quot] [rel_refl] [trans2] rsp_thms *}
+ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac lthy rty [quot] [rel_refl] [trans2] rsp_thms *}
 
 lemma "FOLD f g (z::'b) (INSERT a x) =
   (if rsp_fold f then if IN a x then FOLD f g z x else f (g a) (FOLD f g z x) else z)"
@@ -445,7 +445,6 @@
   done
 
 ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac lthy rty [quot] [rel_refl] [trans2] rsp_thms *}
-ML {* fun inj_repabs_tac_fset' lthy = inj_repabs_tac' lthy rty [quot] [rel_refl] [trans2] rsp_thms *}
 
 (* Construction site starts here *)
 lemma "P (x :: 'a list) (EMPTY :: 'c fset) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT e t)) \<Longrightarrow> P x l"
diff -r f1c0a66284d3 -r 84ee3973f083 IntEx.thy
--- a/IntEx.thy	Sat Nov 28 14:33:04 2009 +0100
+++ b/IntEx.thy	Sat Nov 28 14:45:22 2009 +0100
@@ -142,8 +142,7 @@
 
 ML {* fun lift_tac_intex lthy t = lift_tac lthy t [rel_eqv] rty [quot] rsp_thms defs *}
 
-
-ML {* fun inj_repabs_tac_intex lthy = inj_repabs_tac' lthy rty [quot] [rel_refl] [trans2] rsp_thms *}
+ML {* fun inj_repabs_tac_intex lthy = inj_repabs_tac lthy rty [quot] [rel_refl] [trans2] rsp_thms *}
 ML {* fun all_inj_repabs_tac_intex lthy = all_inj_repabs_tac lthy rty [quot] [rel_refl] [trans2] rsp_thms *}
 
 
diff -r f1c0a66284d3 -r 84ee3973f083 LFex.thy
--- a/LFex.thy	Sat Nov 28 14:33:04 2009 +0100
+++ b/LFex.thy	Sat Nov 28 14:45:22 2009 +0100
@@ -297,7 +297,7 @@
 apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*})
 apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*})
 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 []) 1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
@@ -317,14 +317,14 @@
 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 []) 1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 []) 1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 []) 1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 []) 1*})
-apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 @{thms kpi_rsp}) 1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 @{thms kpi_rsp} 1*})
 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
@@ -347,18 +347,18 @@
 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 []) 1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 []) 1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 @{thms perm_kind_rsp}) 1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 @{thms perm_kind_rsp} 1*})
 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 @{thms perm_kind_rsp}) 1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 @{thms perm_kind_rsp} 1*})
 apply(tactic {* inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms fv_ty_rsp}) 1*})
-apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 @{thms kpi_rsp fv_ty_rsp fv_kind_rsp}) 1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms fv_ty_rsp} 1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 @{thms kpi_rsp fv_ty_rsp fv_kind_rsp} 1*})
 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms tconst_rsp}) 1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms tconst_rsp} 1*})
 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
@@ -375,28 +375,28 @@
 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms fv_ty_rsp}) 1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms fv_ty_rsp} 1*})
 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms fv_ty_rsp}) 1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms fv_ty_rsp} 1*})
 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms fv_ty_rsp}) 1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms fv_ty_rsp} 1*})
 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 @{thms fv_ty_rsp}) 1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 @{thms fv_ty_rsp} 1*})
 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
 apply(tactic {* inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms fv_ty_rsp}) 1*})
-apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms tapp_rsp}) 1*})
-apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms tapp_rsp}) 1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms fv_ty_rsp} 1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms tapp_rsp} 1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms tapp_rsp} 1*})
 apply(tactic {* inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms tpi_rsp}) 1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms tpi_rsp} 1*})
 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms perm_ty_rsp tpi_rsp fv_ty_rsp}) 1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms perm_ty_rsp tpi_rsp fv_ty_rsp} 1*})
 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 @{thms const_rsp}) 1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 @{thms const_rsp} 1*})
 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 @{thms var_rsp}) 1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 @{thms var_rsp} 1*})
 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 @{thms app_rsp}) 1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 @{thms app_rsp} 1*})
 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
@@ -416,10 +416,10 @@
 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 []) 1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 []) 1*})
-apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 @{thms lam_rsp}) 1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 @{thms lam_rsp} 1*})
 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
@@ -445,21 +445,21 @@
 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 []) 1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 []) 1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 @{thms perm_trm_rsp}) 1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 @{thms perm_trm_rsp} 1*})
 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 @{thms perm_trm_rsp}) 1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 @{thms perm_trm_rsp} 1*})
 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms fv_ty_rsp}) 1*})
-apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 @{thms fv_trm_rsp lam_rsp}) 1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 @{thms fv_ty_rsp} 1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 @{thms fv_trm_rsp lam_rsp} 1*})
 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 []) 1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ kind} quot rel_refl trans2 [] 1*})
 apply(tactic {* inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 [] 1*})
-apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 []) 1*})
-apply(tactic {* REPEAT_ALL_NEW (inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 []) 1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ ty} quot rel_refl trans2 [] 1*})
+apply(tactic {* all_inj_repabs_tac @{context} @{typ trm} quot rel_refl trans2 [] 1*})
 done
 
 print_quotients
diff -r f1c0a66284d3 -r 84ee3973f083 QuotMain.thy
--- a/QuotMain.thy	Sat Nov 28 14:33:04 2009 +0100
+++ b/QuotMain.thy	Sat Nov 28 14:45:22 2009 +0100
@@ -877,32 +877,6 @@
 fun SOLVES' tac = tac THEN_ALL_NEW (fn _ => no_tac)
 *}
 
-ML {*
-fun inj_repabs_tac ctxt rty quot_thms rel_refl trans2 rsp_thms =
-  (FIRST' [resolve_tac trans2,
-           lambda_res_tac ctxt,
-           rtac @{thm RES_FORALL_RSP},
-           ball_rsp_tac ctxt,
-           rtac @{thm RES_EXISTS_RSP},
-           bex_rsp_tac ctxt,
-           resolve_tac rsp_thms,
-           rtac @{thm refl},
-           (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' 
-              (RANGE [SOLVES' (quotient_tac quot_thms)])),
-           (APPLY_RSP_TAC rty ctxt THEN' 
-              (RANGE [SOLVES' (quotient_tac quot_thms), SOLVES' (quotient_tac quot_thms)])),
-           Cong_Tac.cong_tac @{thm cong},
-           rtac @{thm ext},
-           resolve_tac rel_refl,
-           atac,
-           (*seems not necessary:: SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps})),*)
-           weak_lambda_res_tac ctxt,
-           CHANGED o (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ}))])
-
-fun all_inj_repabs_tac ctxt rty quot_thms rel_refl trans2 rsp_thms =
-  REPEAT_ALL_NEW (inj_repabs_tac ctxt rty quot_thms rel_refl trans2 rsp_thms)
-*}
-
 (*
 To prove that the regularised theorem implies the abs/rep injected, 
 we try:
@@ -927,71 +901,71 @@
 *)
 
 ML {*
-fun inj_repabs_tac' ctxt rty quot_thms rel_refl trans2 rsp_thms =
+fun inj_repabs_tac ctxt rty quot_thms rel_refl trans2 rsp_thms =
   (FIRST' [
-    (K (print_tac "start")) THEN' (K no_tac), 
+    (*(K (print_tac "start")) THEN' (K no_tac), *)
   
     (* "cong" rule of the of the relation *)
     (* a \<approx> b = c \<approx> d ----> \<lbrakk>a \<approx> c; b \<approx> d\<rbrakk> *)
-    DT ctxt "1" (resolve_tac trans2),
+    NDT ctxt "1" (resolve_tac trans2),
 
     (* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>y\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *) 
-    DT ctxt "2" (lambda_res_tac ctxt),
+    NDT ctxt "2" (lambda_res_tac ctxt),
 
     (* (op =) (Ball\<dots>) (Ball\<dots>) ----> (op =) (\<dots>) (\<dots>) *)
-    DT ctxt "3" (rtac @{thm RES_FORALL_RSP}),
+    NDT ctxt "3" (rtac @{thm RES_FORALL_RSP}),
 
     (* (R1 ===> R2) (Ball\<dots>) (Ball\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (Ball\<dots>x) (Ball\<dots>y) *)
-    DT ctxt "4" (ball_rsp_tac ctxt),
+    NDT ctxt "4" (ball_rsp_tac ctxt),
 
     (* (op =) (Bex\<dots>) (Bex\<dots>) ----> (op =) (\<dots>) (\<dots>) *)
-    DT ctxt "5" (rtac @{thm RES_EXISTS_RSP}),
+    NDT ctxt "5" (rtac @{thm RES_EXISTS_RSP}),
 
     (* (R1 ===> R2) (Bex\<dots>) (Bex\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (Bex\<dots>x) (Bex\<dots>y) *)
-    DT ctxt "6" (bex_rsp_tac ctxt),
+    NDT ctxt "6" (bex_rsp_tac ctxt),
 
     (* respectfulness of constants *)
-    DT ctxt "7" (resolve_tac rsp_thms),
+    NDT ctxt "7" (resolve_tac rsp_thms),
 
     (* reflexivity of operators arising from Cong_tac *)
-    DT ctxt "8" (rtac @{thm refl}),
+    NDT ctxt "8" (rtac @{thm refl}),
 
     (* R (\<dots>) (Rep (Abs \<dots>)) ----> R (\<dots>) (\<dots>) *)
     (* observe ---> *) 
-    DT ctxt "9" ((instantiate_tac @{thm REP_ABS_RSP(1)} ctxt 
+    NDT ctxt "9" ((instantiate_tac @{thm REP_ABS_RSP(1)} ctxt 
                   THEN' (RANGE [SOLVES' (quotient_tac quot_thms)]))),
 
     (* R (t $ \<dots>) (t' $ \<dots>) \<Longrightarrow> APPLY_RSP   provided type of t needs lifting *)
-    DT ctxt "A" ((APPLY_RSP_TAC rty ctxt THEN' 
+    NDT ctxt "A" ((APPLY_RSP_TAC rty ctxt THEN' 
                 (RANGE [SOLVES' (quotient_tac quot_thms), SOLVES' (quotient_tac quot_thms)]))),
 
     (* (op =) (t $ \<dots>) (t' $ \<dots>) \<Longrightarrow> Cong   provided type of t does not need lifting *)
     (* merge with previous tactic *)
-    DT ctxt "B" (Cong_Tac.cong_tac @{thm cong}),
+    NDT ctxt "B" (Cong_Tac.cong_tac @{thm cong}),
 
     (* (op =) (\<lambda>x\<dots>) (\<lambda>x\<dots>) ----> (op =) (\<dots>) (\<dots>) *)
-    DT ctxt "C" (rtac @{thm ext}),
+    NDT ctxt "C" (rtac @{thm ext}),
     
     (* reflexivity of the basic relations *)
-    DT ctxt "D" (resolve_tac rel_refl),
+    NDT ctxt "D" (resolve_tac rel_refl),
 
     (* resolving with R x y assumptions *)
-    DT ctxt "E" (atac),
+    NDT ctxt "E" (atac),
 
-    (* seems not necessay:: DT ctxt "F" (SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))),*)
+    (* seems not necessay:: NDT ctxt "F" (SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))),*)
     
     (* (R1 ===> R2) (\<dots>) (\<lambda>y\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *) 
     (* (R1 ===> R2) (\<lambda>x\<dots>) (\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *) 
-    DT ctxt "G" (weak_lambda_res_tac ctxt),
+    NDT ctxt "G" (weak_lambda_res_tac ctxt),
 
     (* (op =) ===> (op =)  \<Longrightarrow> (op =), needed in order to apply respectfulness theorems *)
     (* global simplification *)
-    DT ctxt "H" (CHANGED o (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ})))])
+    NDT ctxt "H" (CHANGED o (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ})))])
 *}
 
 ML {*
-fun all_inj_repabs_tac' ctxt rty quot_thms rel_refl trans2 rsp_thms =
-  REPEAT_ALL_NEW (inj_repabs_tac' ctxt rty quot_thms rel_refl trans2 rsp_thms)
+fun all_inj_repabs_tac ctxt rty quot_thms rel_refl trans2 rsp_thms =
+  REPEAT_ALL_NEW (inj_repabs_tac ctxt rty quot_thms rel_refl trans2 rsp_thms)
 *}