--- a/QuotMain.thy	Sat Nov 28 03:07:38 2009 +0100
+++ b/QuotMain.thy	Sat Nov 28 04:37:04 2009 +0100
@@ -746,23 +746,20 @@
 using a by (simp add: FUN_REL.simps)
 
 ML {*
-val LAMBDA_RES_TAC =
-  SUBGOAL (fn (goal, i) =>
-    case goal of
-       (_ $ (_ $ (Abs _) $ (Abs _))) => rtac @{thm FUN_REL_I} i
+val LAMBDA_RES_TAC2 =
+  Subgoal.FOCUS (fn {concl, ...} =>
+    case (term_of concl) of
+       (_ $ (_ $ (Abs _) $ (Abs _))) => rtac @{thm FUN_REL_I} 1
      | _ => no_tac)
 *}
 
 ML {*
-fun WEAK_LAMBDA_RES_TAC ctxt i st =
-  (case (term_of o #concl o fst) (Subgoal.focus ctxt i st) of
-    (_ $ (_ $ _ $ (Abs(_, _, _)))) =>
-      (EqSubst.eqsubst_tac ctxt [0] @{thms FUN_REL.simps}) THEN'
-      (rtac @{thm allI}) THEN' (rtac @{thm allI}) THEN' (rtac @{thm impI})
-  | (_ $ (_ $ (Abs(_, _, _)) $ _)) =>
-      (EqSubst.eqsubst_tac ctxt [0] @{thms FUN_REL.simps}) THEN'
-      (rtac @{thm allI}) THEN' (rtac @{thm allI}) THEN' (rtac @{thm impI})
-  | _ => fn _ => no_tac) i st
+val WEAK_LAMBDA_RES_TAC2 =
+  Subgoal.FOCUS (fn {concl, ...} =>
+    case (term_of concl) of
+       (_ $ (_ $ _ $ (Abs _))) => rtac @{thm FUN_REL_I} 1
+     | (_ $ (_ $ (Abs _) $ _)) => rtac @{thm FUN_REL_I} 1
+     | _ => no_tac)
 *}
 
 ML {* (* Legacy *)
@@ -776,14 +773,14 @@
 
 ML {*
 fun APPLY_RSP_TAC rty = 
-  CSUBGOAL (fn (concl, i) =>
+  Subgoal.FOCUS (fn {concl, ...} =>
   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}) i
+    if needs_lift rty (type_of f) then
+      rtac (Drule.instantiate insts @{thm APPLY_RSP}) 1
     else no_tac
   end
   handle _ => no_tac)
@@ -822,7 +819,7 @@
 ML {*
 fun r_mk_comb_tac ctxt rty quot_thms rel_refl trans2 rsp_thms =
   (FIRST' [resolve_tac trans2,
-           LAMBDA_RES_TAC,
+           LAMBDA_RES_TAC2 ctxt,
            rtac @{thm RES_FORALL_RSP},
            ball_rsp_tac ctxt,
            rtac @{thm RES_EXISTS_RSP},
@@ -831,14 +828,14 @@
            rtac @{thm refl},
            (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' 
               (RANGE [SOLVES' (quotient_tac quot_thms)])),
-           (APPLY_RSP_TAC rty THEN' 
+           (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,
+           WEAK_LAMBDA_RES_TAC2 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 =
@@ -878,7 +875,7 @@
     DT ctxt "1" (resolve_tac trans2),
 
     (* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>\<dots>) \<Longrightarrow> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *) 
-    DT ctxt "2" (LAMBDA_RES_TAC),
+    DT ctxt "2" (LAMBDA_RES_TAC2 ctxt),
 
     (* R (Ball\<dots>) (Ball\<dots>) \<Longrightarrow> R (\<dots>) (\<dots>) *)
     DT ctxt "3" (rtac @{thm RES_FORALL_RSP}),
@@ -899,7 +896,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 THEN' 
+    DT ctxt "A" ((APPLY_RSP_TAC rty ctxt 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,7 +912,7 @@
     DT ctxt "E" (atac),
 
     DT ctxt "F" (SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))),
-    DT ctxt "G" (WEAK_LAMBDA_RES_TAC ctxt),
+    DT ctxt "G" (WEAK_LAMBDA_RES_TAC2 ctxt),
     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 =