--- a/Quot/QuotMain.thy	Thu Dec 10 04:23:13 2009 +0100
+++ b/Quot/QuotMain.thy	Thu Dec 10 04:34:24 2009 +0100
@@ -225,20 +225,6 @@
   Seq.single thm
 end *}
 
-ML {*
-fun DT ctxt s tac i thm =
-let
-  val before_goal = nth (prems_of thm) (i - 1)
-                    |> Syntax.string_of_term ctxt
-  val before_msg = ["before: " ^ s, before_goal, "after: " ^ s]
-                   |> cat_lines
-in 
-  EVERY [tac i, my_print_tac ctxt before_msg i] thm
-end
-
-fun NDT ctxt s tac thm = tac thm  
-*}
-
 section {* Matching of Terms and Types *}
 
 ML {*
@@ -866,27 +852,26 @@
 ML {*
 fun inj_repabs_step_tac ctxt rel_refl =
   (FIRST' [
-    NDT ctxt "0" (inj_repabs_tac_match ctxt),
+    inj_repabs_tac_match ctxt,
     (* R (t $ \<dots>) (t' $ \<dots>) ----> apply_rsp   provided type of t needs lifting *)
     
-    NDT ctxt "A" (apply_rsp_tac ctxt THEN'
-                 RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)]),
+    apply_rsp_tac ctxt THEN'
+                 RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)],
 
     (* (op =) (t $ \<dots>) (t' $ \<dots>) ----> Cong   provided type of t does not need lifting *)
     (* merge with previous tactic *)
-    NDT ctxt "C" (Cong_Tac.cong_tac @{thm cong} THEN'
-                (RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)])),
+    Cong_Tac.cong_tac @{thm cong} THEN'
+                 RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)],
     
     (* (op =) (\<lambda>x\<dots>) (\<lambda>x\<dots>) ----> (op =) (\<dots>) (\<dots>) *)
-    NDT ctxt "D" (rtac @{thm ext} THEN' quot_true_tac ctxt unlam),
+    rtac @{thm ext} THEN' quot_true_tac ctxt unlam,
     
     (* resolving with R x y assumptions *)
-    NDT ctxt "E" (atac),
+    atac,
     
     (* reflexivity of the basic relations *)
     (* R \<dots> \<dots> *)
-    NDT ctxt "F" (resolve_tac rel_refl)
-    ])
+    resolve_tac rel_refl])
 *}
 
 ML {*