src/HOL/TPTP/TPTP_Proof_Reconstruction.thy
changeset 59621 291934bac95e
parent 59582 0fbed69ff081
child 59639 f596ed647018
     1.1 --- a/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Fri Mar 06 14:01:08 2015 +0100
     1.2 +++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Fri Mar 06 15:58:56 2015 +0100
     1.3 @@ -917,7 +917,7 @@
     1.4      (* val contextualise = fold absdummy (map snd params) *)
     1.5      val contextualise = fold absfree params
     1.6  
     1.7 -    val skolem_cts = map (contextualise #> Thm.cterm_of thy) skolem_terms
     1.8 +    val skolem_cts = map (contextualise #> Thm.global_cterm_of thy) skolem_terms
     1.9  
    1.10  
    1.11  (*now the instantiation code*)
    1.12 @@ -937,7 +937,7 @@
    1.13          fun make_var pre_var =
    1.14            the_single pre_var
    1.15            |> Var
    1.16 -          |> Thm.cterm_of thy
    1.17 +          |> Thm.global_cterm_of thy
    1.18            |> SOME
    1.19        in
    1.20          if null pre_var then NONE
    1.21 @@ -2003,7 +2003,7 @@
    1.22       thy
    1.23       prob_name (#meta pannot) n
    1.24        |> the
    1.25 -      |> (fn {inference_fmla, ...} => Thm.cterm_of thy inference_fmla)
    1.26 +      |> (fn {inference_fmla, ...} => Thm.global_cterm_of thy inference_fmla)
    1.27        |> oracle_iinterp
    1.28    end
    1.29  *}