--- 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)
 *}