src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
changeset 42361 23f352990944
parent 42284 326f57825e1a
child 42364 8c674b3b8e44
     1.1 --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Sat Apr 16 15:47:52 2011 +0200
     1.2 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Sat Apr 16 16:15:37 2011 +0200
     1.3 @@ -3012,7 +3012,7 @@
     1.4   THEN (fn st =>
     1.5    let
     1.6      val g = List.nth (cprems_of st, i - 1)
     1.7 -    val thy = ProofContext.theory_of ctxt
     1.8 +    val thy = Proof_Context.theory_of ctxt
     1.9      val fs = subtract (op aconv) (map Free (Term.add_frees (term_of g) [])) ps
    1.10      val th = frpar_oracle (T, fs,ps, (* Pattern.eta_long [] *)g)
    1.11    in rtac (th RS iffD2) i st end);
    1.12 @@ -3022,7 +3022,7 @@
    1.13   THEN (fn st =>
    1.14    let
    1.15      val g = List.nth (cprems_of st, i - 1)
    1.16 -    val thy = ProofContext.theory_of ctxt
    1.17 +    val thy = Proof_Context.theory_of ctxt
    1.18      val fs = subtract (op aconv) (map Free (Term.add_frees (term_of g) [])) ps
    1.19      val th = frpar_oracle2 (T, fs,ps, (* Pattern.eta_long [] *)g)
    1.20    in rtac (th RS iffD2) i st end);