src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
changeset 42368 3b8498ac2314
parent 42364 8c674b3b8e44
child 42814 5af15f1e2ef6
     1.1 --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Sat Apr 16 20:30:44 2011 +0200
     1.2 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Sat Apr 16 20:49:48 2011 +0200
     1.3 @@ -3007,25 +3007,23 @@
     1.4  structure FRParTac = 
     1.5  struct
     1.6  
     1.7 -fun frpar_tac T ps ctxt i = 
     1.8 - Object_Logic.full_atomize_tac i
     1.9 - THEN (fn st =>
    1.10 +fun frpar_tac T ps ctxt = 
    1.11 + Object_Logic.full_atomize_tac
    1.12 + THEN' CSUBGOAL (fn (g, i) =>
    1.13    let
    1.14 -    val g = nth (cprems_of st) (i - 1)
    1.15      val thy = Proof_Context.theory_of ctxt
    1.16      val fs = subtract (op aconv) (map Free (Term.add_frees (term_of g) [])) ps
    1.17 -    val th = frpar_oracle (T, fs,ps, (* Pattern.eta_long [] *)g)
    1.18 -  in rtac (th RS iffD2) i st end);
    1.19 +    val th = frpar_oracle (T, fs, ps, (* Pattern.eta_long [] *) g)
    1.20 +  in rtac (th RS iffD2) i end);
    1.21  
    1.22 -fun frpar2_tac T ps ctxt i = 
    1.23 - Object_Logic.full_atomize_tac i
    1.24 - THEN (fn st =>
    1.25 +fun frpar2_tac T ps ctxt = 
    1.26 + Object_Logic.full_atomize_tac
    1.27 + THEN' CSUBGOAL (fn (g, i) =>
    1.28    let
    1.29 -    val g = nth (cprems_of st) (i - 1)
    1.30      val thy = Proof_Context.theory_of ctxt
    1.31      val fs = subtract (op aconv) (map Free (Term.add_frees (term_of g) [])) ps
    1.32 -    val th = frpar_oracle2 (T, fs,ps, (* Pattern.eta_long [] *)g)
    1.33 -  in rtac (th RS iffD2) i st end);
    1.34 +    val th = frpar_oracle2 (T, fs, ps, (* Pattern.eta_long [] *) g)
    1.35 +  in rtac (th RS iffD2) i end);
    1.36  
    1.37  end;
    1.38