proper subgoal addressing via SUBGOAL/CSUBGOAL -- assuming these tactics did not handle Subscript in any special way;
tuned;

--- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Sat Apr 16 20:30:44 2011 +0200
+++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Sat Apr 16 20:49:48 2011 +0200
@@ -3007,25 +3007,23 @@
 structure FRParTac = 
 struct
 
-fun frpar_tac T ps ctxt i = 
- Object_Logic.full_atomize_tac i
- THEN (fn st =>
+fun frpar_tac T ps ctxt = 
+ Object_Logic.full_atomize_tac
+ THEN' CSUBGOAL (fn (g, i) =>
   let
-    val g = nth (cprems_of st) (i - 1)
     val thy = Proof_Context.theory_of ctxt
     val fs = subtract (op aconv) (map Free (Term.add_frees (term_of g) [])) ps
-    val th = frpar_oracle (T, fs,ps, (* Pattern.eta_long [] *)g)
-  in rtac (th RS iffD2) i st end);
+    val th = frpar_oracle (T, fs, ps, (* Pattern.eta_long [] *) g)
+  in rtac (th RS iffD2) i end);
 
-fun frpar2_tac T ps ctxt i = 
- Object_Logic.full_atomize_tac i
- THEN (fn st =>
+fun frpar2_tac T ps ctxt = 
+ Object_Logic.full_atomize_tac
+ THEN' CSUBGOAL (fn (g, i) =>
   let
-    val g = nth (cprems_of st) (i - 1)
     val thy = Proof_Context.theory_of ctxt
     val fs = subtract (op aconv) (map Free (Term.add_frees (term_of g) [])) ps
-    val th = frpar_oracle2 (T, fs,ps, (* Pattern.eta_long [] *)g)
-  in rtac (th RS iffD2) i st end);
+    val th = frpar_oracle2 (T, fs, ps, (* Pattern.eta_long [] *) g)
+  in rtac (th RS iffD2) i end);
 
 end;
 

--- a/src/HOL/Decision_Procs/cooper_tac.ML	Sat Apr 16 20:30:44 2011 +0200
+++ b/src/HOL/Decision_Procs/cooper_tac.ML	Sat Apr 16 20:49:48 2011 +0200
@@ -66,9 +66,8 @@
 fun mp_step n th = if (n=0) then th else (mp_step (n-1) th) RS mp;
 
 
-fun linz_tac ctxt q i = Object_Logic.atomize_prems_tac i THEN (fn st =>
+fun linz_tac ctxt q = Object_Logic.atomize_prems_tac THEN' SUBGOAL (fn (g, i) =>
   let
-    val g = nth (prems_of st) (i - 1)
     val thy = Proof_Context.theory_of ctxt
     (* Transform the term*)
     val (t,np,nh) = prepare_for_linz q g
@@ -117,9 +116,7 @@
             assm_tac (i + 1) THEN (if q then I else TRY) (rtac TrueI i))
     end
       | _ => (pre_thm, assm_tac i)
-  in (rtac (((mp_step nh) o (spec_step np)) th) i
-      THEN tac) st
-  end handle Subscript => no_tac st);
+  in rtac (((mp_step nh) o (spec_step np)) th) i THEN tac end);
 
 val setup =
   Method.setup @{binding cooper}

--- a/src/HOL/Decision_Procs/mir_tac.ML	Sat Apr 16 20:30:44 2011 +0200
+++ b/src/HOL/Decision_Procs/mir_tac.ML	Sat Apr 16 20:49:48 2011 +0200
@@ -87,13 +87,12 @@
 fun mp_step n th = if (n=0) then th else (mp_step (n-1) th) RS mp;
 
 
-fun mir_tac ctxt q i = 
-    Object_Logic.atomize_prems_tac i
-        THEN simp_tac (HOL_basic_ss addsimps [@{thm "abs_ge_zero"}] addsimps simp_thms) i
-        THEN REPEAT_DETERM (split_tac [@{thm "split_min"}, @{thm "split_max"}, @{thm "abs_split"}] i)
-        THEN (fn st =>
+fun mir_tac ctxt q = 
+    Object_Logic.atomize_prems_tac
+        THEN' simp_tac (HOL_basic_ss addsimps [@{thm "abs_ge_zero"}] addsimps simp_thms)
+        THEN' (REPEAT_DETERM o split_tac [@{thm "split_min"}, @{thm "split_max"}, @{thm "abs_split"}])
+        THEN' SUBGOAL (fn (g, i) =>
   let
-    val g = nth (prems_of st) (i - 1)
     val thy = Proof_Context.theory_of ctxt
     (* Transform the term*)
     val (t,np,nh) = prepare_for_mir thy q g
@@ -145,9 +144,7 @@
             assm_tac (i + 1) THEN (if q then I else TRY) (rtac TrueI i)))
     end
       | _ => (pre_thm, assm_tac i)
-  in (rtac (((mp_step nh) o (spec_step np)) th) i 
-      THEN tac) st
-  end handle Subscript => no_tac st);
+  in rtac (((mp_step nh) o (spec_step np)) th) i THEN tac end);
 
 val setup =
   Method.setup @{binding mir}

--- a/src/HOL/Import/shuffler.ML	Sat Apr 16 20:30:44 2011 +0200
+++ b/src/HOL/Import/shuffler.ML	Sat Apr 16 20:49:48 2011 +0200
@@ -606,21 +606,18 @@
         filter (match_consts ignored t) all_thms
     end
 
-fun gen_shuffle_tac ctxt search thms i st =
+fun gen_shuffle_tac ctxt search thms = SUBGOAL (fn (t, i) =>
     let
         val thy = Proof_Context.theory_of ctxt
-        val _ = message ("Shuffling " ^ (string_of_thm st))
-        val t = nth (prems_of st) (i - 1)
         val set = set_prop thy t
         fun process_tac thms st =
             case set thms of
                 SOME (_,th) => Seq.of_list (compose (th,i,st))
               | NONE => Seq.empty
     in
-        (process_tac thms APPEND (if search
-                                  then process_tac (find_potential thy t)
-                                  else no_tac)) st
-    end
+        process_tac thms APPEND
+          (if search then process_tac (find_potential thy t) else no_tac)
+    end)
 
 fun shuffle_tac ctxt thms =
   gen_shuffle_tac ctxt false (map (pair "") thms);

--- a/src/HOL/Library/reflection.ML	Sat Apr 16 20:30:44 2011 +0200
+++ b/src/HOL/Library/reflection.ML	Sat Apr 16 20:49:48 2011 +0200
@@ -298,23 +298,19 @@
              (simplify (HOL_basic_ss addsimps [rth]) th)
   end
 
-fun genreify_tac ctxt eqs to i = (fn st =>
+fun genreify_tac ctxt eqs to = SUBGOAL (fn (goal, i) =>
   let
-    fun P () = HOLogic.dest_Trueprop (nth (prems_of st) (i - 1))
-    val t = (case to of NONE => P () | SOME x => x)
-    val th = (genreif ctxt eqs t) RS ssubst
-  in rtac th i st
-  end);
+    val t = (case to of NONE => HOLogic.dest_Trueprop goal | SOME x => x)
+    val th = genreif ctxt eqs t RS ssubst
+  in rtac th i end);
 
     (* Reflection calls reification and uses the correctness *)
         (* theorem assumed to be the dead of the list *)
-fun gen_reflection_tac ctxt conv corr_thms raw_eqs to i = (fn st =>
+fun gen_reflection_tac ctxt conv corr_thms raw_eqs to = SUBGOAL (fn (goal, i) =>
   let
-    val P = HOLogic.dest_Trueprop (nth (prems_of st) (i - 1));
-    val t = the_default P to;
-    val th = genreflect ctxt conv corr_thms raw_eqs t
-      RS ssubst;
-  in (rtac th i THEN TRY(rtac TrueI i)) st end);
+    val t = (case to of NONE => HOLogic.dest_Trueprop goal | SOME x => x)
+    val th = genreflect ctxt conv corr_thms raw_eqs t RS ssubst
+  in rtac th i THEN TRY (rtac TrueI i) end);  (* FIXME THEN_ALL_NEW !? *)
 
 fun reflection_tac ctxt = gen_reflection_tac ctxt Codegen.evaluation_conv;
   (*FIXME why Codegen.evaluation_conv?  very specific...*)

--- a/src/HOL/Statespace/distinct_tree_prover.ML	Sat Apr 16 20:30:44 2011 +0200
+++ b/src/HOL/Statespace/distinct_tree_prover.ML	Sat Apr 16 20:49:48 2011 +0200
@@ -13,7 +13,7 @@
   val distinctTreeProver : thm -> Direction list -> Direction list -> thm
   val neq_x_y : Proof.context -> term -> term -> string -> thm option   
   val distinctFieldSolver : string list -> solver
-  val distinctTree_tac : string list -> Proof.context -> term * int -> tactic
+  val distinctTree_tac : string list -> Proof.context -> int -> tactic
   val distinct_implProver : thm -> cterm -> thm
   val subtractProver : term -> cterm -> thm -> thm
   val distinct_simproc : string list -> simproc
@@ -343,17 +343,19 @@
   in SOME thm  
   end handle Option => NONE)
 
-fun distinctTree_tac names ctxt 
-      (Const (@{const_name Trueprop},_) $ (Const (@{const_name Not}, _) $ (Const (@{const_name HOL.eq}, _) $ x $ y)), i) =
-  (case get_fst_success (neq_x_y ctxt x y) names of
-     SOME neq => rtac neq i
-   | NONE => no_tac)
-  | distinctTree_tac _ _ _ = no_tac;
+fun distinctTree_tac names ctxt = SUBGOAL (fn (goal, i) =>
+    (case goal of
+      Const (@{const_name Trueprop}, _) $
+          (Const (@{const_name Not}, _) $ (Const (@{const_name HOL.eq}, _) $ x $ y)) =>
+        (case get_fst_success (neq_x_y ctxt x y) names of
+          SOME neq => rtac neq i
+        | NONE => no_tac)
+    | _ => no_tac))
 
 fun distinctFieldSolver names = mk_solver' "distinctFieldSolver"
      (fn ss => case try Simplifier.the_context ss of
-                 SOME ctxt => SUBGOAL (distinctTree_tac names ctxt)
-                | NONE => fn i => no_tac)
+                 SOME ctxt => distinctTree_tac names ctxt
+               | NONE => K no_tac)
 
 fun distinct_simproc names =
   Simplifier.simproc_global @{theory HOL} "DistinctTreeProver.distinct_simproc" ["x = y"]

--- a/src/HOL/Statespace/state_space.ML	Sat Apr 16 20:30:44 2011 +0200
+++ b/src/HOL/Statespace/state_space.ML	Sat Apr 16 20:49:48 2011 +0200
@@ -39,8 +39,7 @@
 
     val neq_x_y : Proof.context -> term -> term -> thm option
     val distinctNameSolver : Simplifier.solver
-    val distinctTree_tac :
-       Proof.context -> term * int -> Tactical.tactic
+    val distinctTree_tac : Proof.context -> int -> tactic
     val distinct_simproc : Simplifier.simproc
 
 
@@ -221,18 +220,20 @@
   in SOME thm
   end handle Option => NONE)
 
-fun distinctTree_tac ctxt
-      (Const (@{const_name Trueprop},_) $
-        (Const (@{const_name Not}, _) $ (Const (@{const_name HOL.eq}, _) $ (x as Free _)$ (y as Free _))), i) =
-  (case (neq_x_y ctxt x y) of
-     SOME neq => rtac neq i
-   | NONE => no_tac)
-  | distinctTree_tac _ _ = no_tac;
+fun distinctTree_tac ctxt = SUBGOAL (fn (goal, i) =>
+  (case goal of
+    Const (@{const_name Trueprop}, _) $
+      (Const (@{const_name Not}, _) $
+        (Const (@{const_name HOL.eq}, _) $ (x as Free _) $ (y as Free _))) =>
+      (case neq_x_y ctxt x y of
+        SOME neq => rtac neq i
+      | NONE => no_tac)
+  | _ => no_tac));
 
 val distinctNameSolver = mk_solver' "distinctNameSolver"
      (fn ss => case try Simplifier.the_context ss of
-                 SOME ctxt => SUBGOAL (distinctTree_tac ctxt)
-                | NONE => fn i => no_tac)
+                 SOME ctxt => distinctTree_tac ctxt
+                | NONE => K no_tac)
 
 val distinct_simproc =
   Simplifier.simproc_global @{theory HOL} "StateSpace.distinct_simproc" ["x = y"]
@@ -249,16 +250,14 @@
 fun interprete_parent name dist_thm_name parent_expr thy =
   let
 
-    fun solve_tac ctxt (_,i) st =
+    fun solve_tac ctxt = CSUBGOAL (fn (goal, i) =>
       let
         val distinct_thm = Proof_Context.get_thm ctxt dist_thm_name;
-        val goal = nth (cprems_of st) (i - 1);
         val rule = DistinctTreeProver.distinct_implProver distinct_thm goal;
-      in EVERY [rtac rule i] st
-      end
+      in rtac rule i end);
 
-    fun tac ctxt = EVERY [Locale.intro_locales_tac true ctxt [],
-                          ALLGOALS (SUBGOAL (solve_tac ctxt))]
+    fun tac ctxt =
+      Locale.intro_locales_tac true ctxt [] THEN ALLGOALS (solve_tac ctxt);
 
   in thy
      |> prove_interpretation_in tac (name,parent_expr)

--- a/src/HOL/Tools/Datatype/datatype_aux.ML	Sat Apr 16 20:30:44 2011 +0200
+++ b/src/HOL/Tools/Datatype/datatype_aux.ML	Sat Apr 16 20:49:48 2011 +0200
@@ -128,44 +128,49 @@
 
 (* instantiate induction rule *)
 
-fun indtac indrule indnames i st =
+fun indtac indrule indnames = CSUBGOAL (fn (cgoal, i) =>
   let
+    val cert = cterm_of (Thm.theory_of_cterm cgoal);
+    val goal = term_of cgoal;
     val ts = HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of indrule));
-    val ts' = HOLogic.dest_conj (HOLogic.dest_Trueprop
-      (Logic.strip_imp_concl (nth (prems_of st) (i - 1))));
-    val getP = if can HOLogic.dest_imp (hd ts) then
-      (apfst SOME) o HOLogic.dest_imp else pair NONE;
-    val flt = if null indnames then I else
-      filter (fn Free (s, _) => member (op =) indnames s | _ => false);
-    fun abstr (t1, t2) = (case t1 of
-        NONE => (case flt (OldTerm.term_frees t2) of
+    val ts' = HOLogic.dest_conj (HOLogic.dest_Trueprop (Logic.strip_imp_concl goal));
+    val getP =
+      if can HOLogic.dest_imp (hd ts)
+      then apfst SOME o HOLogic.dest_imp
+      else pair NONE;
+    val flt =
+      if null indnames then I
+      else filter (fn Free (s, _) => member (op =) indnames s | _ => false);
+    fun abstr (t1, t2) =
+      (case t1 of
+        NONE =>
+          (case flt (OldTerm.term_frees t2) of
             [Free (s, T)] => SOME (absfree (s, T, t2))
           | _ => NONE)
       | SOME (_ $ t') => SOME (Abs ("x", fastype_of t', abstract_over (t', t2))))
-    val cert = cterm_of (Thm.theory_of_thm st);
-    val insts = map_filter (fn (t, u) => case abstr (getP u) of
+    val insts = map_filter (fn (t, u) =>
+      case abstr (getP u) of
         NONE => NONE
       | SOME u' => SOME (t |> getP |> snd |> head_of |> cert, cert u')) (ts ~~ ts');
     val indrule' = cterm_instantiate insts indrule
-  in
-    rtac indrule' i st
-  end;
+  in rtac indrule' i end);
+
 
 (* perform exhaustive case analysis on last parameter of subgoal i *)
 
-fun exh_tac exh_thm_of i state =
+fun exh_tac exh_thm_of = CSUBGOAL (fn (cgoal, i) =>
   let
-    val thy = Thm.theory_of_thm state;
-    val prem = nth (prems_of state) (i - 1);
-    val params = Logic.strip_params prem;
+    val thy = Thm.theory_of_cterm cgoal;
+    val goal = term_of cgoal;
+    val params = Logic.strip_params goal;
     val (_, Type (tname, _)) = hd (rev params);
-    val exhaustion = Thm.lift_rule (Thm.cprem_of state i) (exh_thm_of tname);
+    val exhaustion = Thm.lift_rule cgoal (exh_thm_of tname);
     val prem' = hd (prems_of exhaustion);
     val _ $ (_ $ lhs $ _) = hd (rev (Logic.strip_assums_hyp prem'));
-    val exhaustion' = cterm_instantiate [(cterm_of thy (head_of lhs),
-      cterm_of thy (fold_rev (fn (_, T) => fn t => Abs ("z", T, t)) params (Bound 0)))] exhaustion
-  in compose_tac (false, exhaustion', nprems_of exhaustion) i state
-  end;
+    val exhaustion' =
+      cterm_instantiate [(cterm_of thy (head_of lhs),
+        cterm_of thy (fold_rev (fn (_, T) => fn t => Abs ("z", T, t)) params (Bound 0)))] exhaustion
+  in compose_tac (false, exhaustion', nprems_of exhaustion) i end);
 
 
 (********************** Internal description of datatypes *********************)