--- a/QuotMain.thy	Sat Nov 28 02:54:24 2009 +0100
+++ b/QuotMain.thy	Sat Nov 28 03:06:22 2009 +0100
@@ -775,21 +775,23 @@
 *}
 
 ML {*
-fun APPLY_RSP_TAC rty = Subgoal.FOCUS (fn {concl, ...} =>
+fun APPLY_RSP_TAC rty = 
+  CSUBGOAL (fn (concl, i) =>
   let
     val (_ $ (R $ (f $ _) $ (_ $ _))) = term_of concl;
     val pat = Drule.strip_imp_concl (cprop_of @{thm APPLY_RSP});
     val insts = Thm.match (pat, concl)
   in
-    if needs_lift rty (type_of f) then
-      rtac (Drule.instantiate insts @{thm APPLY_RSP}) 1
+    if needs_lift rty (type_of f) 
+    then rtac (Drule.instantiate insts @{thm APPLY_RSP}) i
     else no_tac
   end
   handle _ => no_tac)
 *}
 
 ML {*
-val ball_rsp_tac = Subgoal.FOCUS (fn {concl, context = ctxt, ...} =>
+val ball_rsp_tac = 
+  Subgoal.FOCUS (fn {concl, context = ctxt, ...} =>
   let
     val _ $ (_ $ (Const (@{const_name Ball}, _) $ _) $
                  (Const (@{const_name Ball}, _) $ _)) = term_of concl
@@ -803,7 +805,8 @@
 *}
 
 ML {*
-val bex_rsp_tac = Subgoal.FOCUS (fn {concl, context = ctxt, ...} =>
+val bex_rsp_tac = 
+  Subgoal.FOCUS (fn {concl, context = ctxt, ...} =>
   let
     val _ $ (_ $ (Const (@{const_name Bex}, _) $ _) $
                  (Const (@{const_name Bex}, _) $ _)) = term_of concl
@@ -818,27 +821,25 @@
 
 ML {*
 fun r_mk_comb_tac ctxt rty quot_thms rel_refl trans2 rsp_thms =
-  (FIRST' [
-    resolve_tac trans2,
-    LAMBDA_RES_TAC,
-    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,
-    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}))
-    ])
+  (FIRST' [resolve_tac trans2,
+           LAMBDA_RES_TAC,
+           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 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,
+           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_r_mk_comb_tac ctxt rty quot_thms rel_refl trans2 rsp_thms =
   REPEAT_ALL_NEW (r_mk_comb_tac ctxt rty quot_thms rel_refl trans2 rsp_thms)
@@ -898,7 +899,7 @@
                   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' 
+    DT ctxt "A" ((APPLY_RSP_TAC rty THEN' 
                 (RANGE [SOLVES' (quotient_tac quot_thms), SOLVES' (quotient_tac quot_thms)]))),
 
     (* R (t $ \<dots>) (t' $ \<dots>) \<Longrightarrow> Cong provided R = (op =) and t does not need lifting *)
@@ -915,8 +916,7 @@
 
     DT ctxt "F" (SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))),
     DT ctxt "G" (WEAK_LAMBDA_RES_TAC ctxt),
-    DT ctxt "H" (CHANGED o (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ})))
-    ])
+    DT ctxt "H" (CHANGED o (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ})))])
 
 fun all_r_mk_comb_tac' ctxt rty quot_thms rel_refl trans2 rsp_thms =
   REPEAT_ALL_NEW (r_mk_comb_tac' ctxt rty quot_thms rel_refl trans2 rsp_thms)