--- a/QuotMain.thy	Sat Nov 28 14:45:22 2009 +0100
+++ b/QuotMain.thy	Sat Nov 28 18:49:39 2009 +0100
@@ -237,19 +237,29 @@
 section {* Debugging infrastructure for testing tactics *}
 
 ML {*
+fun fst_prem_str ctxt [] = "No subgoals" 
+  | fst_prem_str ctxt thms = (hd thms) |> Syntax.string_of_term ctxt
+*}
+
+ML {*
 fun my_print_tac ctxt s thm =
 let
-  val prems_str = prems_of thm
-                  |> map (Syntax.string_of_term ctxt)
-                  |> cat_lines
-  val _ = tracing (s ^ "\n" ^ prems_str)
+  val _ = tracing (s ^ "\n" ^ (fst_prem_str ctxt (prems_of thm)))
 in
   Seq.single thm
 end
+*}
 
-fun DT ctxt s tac = EVERY' [tac, K (my_print_tac ctxt ("after " ^ s))]
+ML {*
+fun DT ctxt s tac i thm =
+   let
+     val fst_goal_start = fst_prem_str ctxt (prems_of thm)
+   in 
+     EVERY [tac i,
+            my_print_tac ctxt (cat_lines ["before: " ^ s, fst_goal_start, "after: " ^ s])] thm  
+   end
 
-fun NDT ctxt s tac = tac
+fun NDT ctxt s tac thm = tac thm  
 *}
 
 section {*  Infrastructure about definitions *}
@@ -903,8 +913,6 @@
 ML {*
 fun inj_repabs_tac ctxt rty quot_thms rel_refl trans2 rsp_thms =
   (FIRST' [
-    (*(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> *)
     NDT ctxt "1" (resolve_tac trans2),
@@ -913,10 +921,10 @@
     NDT ctxt "2" (lambda_res_tac ctxt),
 
     (* (op =) (Ball\<dots>) (Ball\<dots>) ----> (op =) (\<dots>) (\<dots>) *)
-    NDT ctxt "3" (rtac @{thm RES_FORALL_RSP}),
+    DT 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) *)
-    NDT ctxt "4" (ball_rsp_tac ctxt),
+    DT ctxt "4" (ball_rsp_tac ctxt),
 
     (* (op =) (Bex\<dots>) (Bex\<dots>) ----> (op =) (\<dots>) (\<dots>) *)
     NDT ctxt "5" (rtac @{thm RES_EXISTS_RSP}),