src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
changeset 42364 8c674b3b8e44
parent 42361 23f352990944
child 42368 3b8498ac2314
     1.1 --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Sat Apr 16 16:37:21 2011 +0200
     1.2 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Sat Apr 16 18:11:20 2011 +0200
     1.3 @@ -3011,7 +3011,7 @@
     1.4   Object_Logic.full_atomize_tac i
     1.5   THEN (fn st =>
     1.6    let
     1.7 -    val g = List.nth (cprems_of st, i - 1)
     1.8 +    val g = nth (cprems_of st) (i - 1)
     1.9      val thy = Proof_Context.theory_of ctxt
    1.10      val fs = subtract (op aconv) (map Free (Term.add_frees (term_of g) [])) ps
    1.11      val th = frpar_oracle (T, fs,ps, (* Pattern.eta_long [] *)g)
    1.12 @@ -3021,7 +3021,7 @@
    1.13   Object_Logic.full_atomize_tac i
    1.14   THEN (fn st =>
    1.15    let
    1.16 -    val g = List.nth (cprems_of st, i - 1)
    1.17 +    val g = nth (cprems_of st) (i - 1)
    1.18      val thy = Proof_Context.theory_of ctxt
    1.19      val fs = subtract (op aconv) (map Free (Term.add_frees (term_of g) [])) ps
    1.20      val th = frpar_oracle2 (T, fs,ps, (* Pattern.eta_long [] *)g)