src/HOL/Decision_Procs/cooper_tac.ML
changeset 42368 3b8498ac2314
parent 42364 8c674b3b8e44
child 43594 ef1ddc59b825
     1.1 --- a/src/HOL/Decision_Procs/cooper_tac.ML	Sat Apr 16 20:30:44 2011 +0200
     1.2 +++ b/src/HOL/Decision_Procs/cooper_tac.ML	Sat Apr 16 20:49:48 2011 +0200
     1.3 @@ -66,9 +66,8 @@
     1.4  fun mp_step n th = if (n=0) then th else (mp_step (n-1) th) RS mp;
     1.5  
     1.6  
     1.7 -fun linz_tac ctxt q i = Object_Logic.atomize_prems_tac i THEN (fn st =>
     1.8 +fun linz_tac ctxt q = Object_Logic.atomize_prems_tac THEN' SUBGOAL (fn (g, i) =>
     1.9    let
    1.10 -    val g = nth (prems_of st) (i - 1)
    1.11      val thy = Proof_Context.theory_of ctxt
    1.12      (* Transform the term*)
    1.13      val (t,np,nh) = prepare_for_linz q g
    1.14 @@ -117,9 +116,7 @@
    1.15              assm_tac (i + 1) THEN (if q then I else TRY) (rtac TrueI i))
    1.16      end
    1.17        | _ => (pre_thm, assm_tac i)
    1.18 -  in (rtac (((mp_step nh) o (spec_step np)) th) i
    1.19 -      THEN tac) st
    1.20 -  end handle Subscript => no_tac st);
    1.21 +  in rtac (((mp_step nh) o (spec_step np)) th) i THEN tac end);
    1.22  
    1.23  val setup =
    1.24    Method.setup @{binding cooper}