src/HOL/TPTP/TPTP_Proof_Reconstruction.thy
changeset 59639 f596ed647018
parent 59621 291934bac95e
child 59755 f8d164ab0dc1
     1.1 --- a/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Fri Mar 06 23:54:05 2015 +0100
     1.2 +++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Fri Mar 06 23:54:36 2015 +0100
     1.3 @@ -806,8 +806,6 @@
     1.4  ML {*
     1.5  fun instantiate_skols ctxt consts_candidates i = fn st =>
     1.6    let
     1.7 -    val thy = Proof_Context.theory_of ctxt
     1.8 -
     1.9      val gls =
    1.10        Thm.prop_of st
    1.11        |> Logic.strip_horn
    1.12 @@ -917,7 +915,7 @@
    1.13      (* val contextualise = fold absdummy (map snd params) *)
    1.14      val contextualise = fold absfree params
    1.15  
    1.16 -    val skolem_cts = map (contextualise #> Thm.global_cterm_of thy) skolem_terms
    1.17 +    val skolem_cts = map (contextualise #> Thm.cterm_of ctxt) skolem_terms
    1.18  
    1.19  
    1.20  (*now the instantiation code*)
    1.21 @@ -937,7 +935,7 @@
    1.22          fun make_var pre_var =
    1.23            the_single pre_var
    1.24            |> Var
    1.25 -          |> Thm.global_cterm_of thy
    1.26 +          |> Thm.cterm_of ctxt
    1.27            |> SOME
    1.28        in
    1.29          if null pre_var then NONE
    1.30 @@ -2003,7 +2001,7 @@
    1.31       thy
    1.32       prob_name (#meta pannot) n
    1.33        |> the
    1.34 -      |> (fn {inference_fmla, ...} => Thm.global_cterm_of thy inference_fmla)
    1.35 +      |> (fn {inference_fmla, ...} => Thm.cterm_of ctxt inference_fmla)
    1.36        |> oracle_iinterp
    1.37    end
    1.38  *}