--- a/QuotMain.thy	Sun Nov 29 02:51:42 2009 +0100
+++ b/QuotMain.thy	Sun Nov 29 03:59:18 2009 +0100
@@ -235,28 +235,30 @@
 
 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 =
+fun my_print_tac ctxt s i thm =
 let
-  val _ = tracing (s ^ "\n" ^ (fst_prem_str ctxt (prems_of thm)))
+  val prem_str = nth (prems_of thm) (i - 1)
+                 |> Syntax.string_of_term ctxt
+                 handle Subscript => "no subgoal"
+  val _ = tracing (s ^ "\n" ^ prem_str)
 in
   Seq.single thm
-end
-*}
+end *}
+
 
 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
+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  
 *}
@@ -892,7 +894,7 @@
 *)
 
 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 =
   (FIRST' [
     (* "cong" rule of the of the relation / transitivity*)
     (* (op =) (R a b) (R c d) ----> \<lbrakk>R a c; R b d\<rbrakk> *)
@@ -914,7 +916,7 @@
     NDT ctxt "6" (bex_rsp_tac ctxt),
 
     (* respectfulness of constants *)
-    DT ctxt "7" (resolve_tac rsp_thms),
+    NDT ctxt "7" (resolve_tac (rsp_rules_get ctxt)),
 
     (* reflexivity of operators arising from Cong_tac *)
     NDT ctxt "8" (rtac @{thm refl}),
@@ -954,8 +956,8 @@
 *}
 
 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 =
+  REPEAT_ALL_NEW (inj_repabs_tac ctxt rty quot_thms rel_refl trans2)
 *}
 
 
@@ -1194,7 +1196,7 @@
 
 ML {*
 (* FIXME/TODO should only get as arguments the rthm like procedure_tac *)
-fun lift_tac lthy rthm rel_eqv rty quot rsp_thms defs =
+fun lift_tac lthy rthm rel_eqv rty quot defs =
   ObjectLogic.full_atomize_tac
   THEN' gen_frees_tac lthy
   THEN' Subgoal.FOCUS (fn {context, concl, ...} =>
@@ -1209,7 +1211,7 @@
        [rtac rule,
         RANGE [rtac rthm',
                regularize_tac lthy rel_eqv,
-               all_inj_repabs_tac lthy rty quot rel_refl trans2 rsp_thms,
+               all_inj_repabs_tac lthy rty quot rel_refl trans2,
                clean_tac lthy quot defs aps]]
     end) lthy
 *}