diff -r 577d85fb5862 -r 3b8498ac2314 src/HOL/Decision_Procs/cooper_tac.ML
--- 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}