src/HOL/Tools/Meson/meson_clausify.ML

   exists (fn prefix => String.isPrefix prefix s)
          [new_skolem_var_prefix, new_nonskolem_var_prefix]
 
 (**** Transformation of Elimination Rules into First-Order Formulas****)
 
-val cfalse = Thm.global_cterm_of @{theory HOL} @{term False};
-val ctp_false = Thm.global_cterm_of @{theory HOL} (HOLogic.mk_Trueprop @{term False});
+val cfalse = Thm.cterm_of @{theory_context HOL} @{term False};
+val ctp_false = Thm.cterm_of @{theory_context HOL} (HOLogic.mk_Trueprop @{term False});
 
 (* Converts an elim-rule into an equivalent theorem that does not have the
    predicate variable. Leaves other theorems unchanged. We simply instantiate
    the conclusion variable to False. (Cf. "transform_elim_prop" in
    "Sledgehammer_Util".) *)
 fun transform_elim_theorem th =
   (case Thm.concl_of th of    (*conclusion variable*)
     @{const Trueprop} $ (v as Var (_, @{typ bool})) =>
-      Thm.instantiate ([], [(Thm.global_cterm_of @{theory HOL} v, cfalse)]) th
+      Thm.instantiate ([], [(Thm.cterm_of @{theory_context HOL} v, cfalse)]) th
   | v as Var(_, @{typ prop}) =>
-      Thm.instantiate ([], [(Thm.global_cterm_of @{theory HOL} v, ctp_false)]) th
+      Thm.instantiate ([], [(Thm.cterm_of @{theory_context HOL} v, ctp_false)]) th
   | _ => th)
 
 
 (**** SKOLEMIZATION BY INFERENCE (lcp) ****)
 

   | is_quasi_lambda_free (t1 $ t2) =
     is_quasi_lambda_free t1 andalso is_quasi_lambda_free t2
   | is_quasi_lambda_free (Abs _) = false
   | is_quasi_lambda_free _ = true
 
-val [f_B,g_B] = map (Thm.global_cterm_of @{theory}) (Misc_Legacy.term_vars (Thm.prop_of @{thm abs_B}));
-val [g_C,f_C] = map (Thm.global_cterm_of @{theory}) (Misc_Legacy.term_vars (Thm.prop_of @{thm abs_C}));
-val [f_S,g_S] = map (Thm.global_cterm_of @{theory}) (Misc_Legacy.term_vars (Thm.prop_of @{thm abs_S}));
+val [f_B,g_B] = map (Thm.cterm_of @{context}) (Misc_Legacy.term_vars (Thm.prop_of @{thm abs_B}));
+val [g_C,f_C] = map (Thm.cterm_of @{context}) (Misc_Legacy.term_vars (Thm.prop_of @{thm abs_C}));
+val [f_S,g_S] = map (Thm.cterm_of @{context}) (Misc_Legacy.term_vars (Thm.prop_of @{thm abs_S}));
 
 (* FIXME: Requires more use of cterm constructors. *)
 fun abstract ct =
   let
       val thy = Thm.theory_of_cterm ct

               "\nException message: " ^ msg);
             (* A type variable of sort "{}" will make "abstraction" fail. *)
             TrueI)
 
 (*cterms are used throughout for efficiency*)
-val cTrueprop = Thm.global_cterm_of @{theory HOL} HOLogic.Trueprop;
+val cTrueprop = Thm.cterm_of @{theory_context HOL} HOLogic.Trueprop;
 
 (*Given an abstraction over n variables, replace the bound variables by free
   ones. Return the body, along with the list of free variables.*)
 fun c_variant_abs_multi (ct0, vars) =
       let val (cv,ct) = Thm.dest_abs NONE ct0

 (* Given the definition of a Skolem function, return a theorem to replace
    an existential formula by a use of that function.
    Example: "EX x. x : A & x ~: B ==> sko A B : A & sko A B ~: B"  [.] *)
 fun old_skolem_theorem_of_def ctxt rhs0 =
   let
-    val thy = Proof_Context.theory_of ctxt
-    val rhs = rhs0 |> Type.legacy_freeze_thaw |> #1 |> Thm.global_cterm_of thy
+    val rhs = rhs0 |> Type.legacy_freeze_thaw |> #1 |> Thm.cterm_of ctxt
     val rhs' = rhs |> Thm.dest_comb |> snd
     val (ch, frees) = c_variant_abs_multi (rhs', [])
     val (hilbert, cabs) = ch |> Thm.dest_comb |>> Thm.term_of
     val T =
       case hilbert of
         Const (_, Type (@{type_name fun}, [_, T])) => T
       | _ => raise TERM ("old_skolem_theorem_of_def: expected \"Eps\"", [hilbert])
-    val cex = Thm.global_cterm_of thy (HOLogic.exists_const T)
+    val cex = Thm.cterm_of ctxt (HOLogic.exists_const T)
     val ex_tm = Thm.apply cTrueprop (Thm.apply cex cabs)
     val conc =
       Drule.list_comb (rhs, frees)
       |> Drule.beta_conv cabs |> Thm.apply cTrueprop
     fun tacf [prem] =
       rewrite_goals_tac ctxt @{thms skolem_def [abs_def]}
-      THEN resolve_tac ctxt [(prem |> rewrite_rule ctxt @{thms skolem_def [abs_def]})
-                 RS Global_Theory.get_thm thy "Hilbert_Choice.someI_ex"] 1
+      THEN resolve_tac ctxt
+        [(prem |> rewrite_rule ctxt @{thms skolem_def [abs_def]})
+          RS Global_Theory.get_thm (Proof_Context.theory_of ctxt) "Hilbert_Choice.someI_ex"] 1
   in
     Goal.prove_internal ctxt [ex_tm] conc tacf
     |> forall_intr_list frees
     |> Thm.forall_elim_vars 0  (*Introduce Vars, but don't discharge defs.*)
     |> Thm.varifyT_global

       th |> transform_elim_theorem
          |> zero_var_indexes
          |> new_skolem ? forall_intr_vars
     val (th, ctxt) = Variable.import true [th] ctxt |>> snd |>> the_single
     val th = th |> Conv.fconv_rule (Object_Logic.atomize ctxt)
-                |> cong_extensionalize_thm thy
+                |> cong_extensionalize_thm ctxt
                 |> abs_extensionalize_thm ctxt
                 |> make_nnf ctxt
   in
     if new_skolem then
       let

         val zapped_th =
           discharger_th |> Thm.prop_of |> rename_bound_vars_to_be_zapped ax_no
           |> (if no_choice then
                 Skip_Proof.make_thm thy #> skolemize [cheat_choice] #> Thm.cprop_of
               else
-                Thm.global_cterm_of thy)
+                Thm.cterm_of ctxt)
           |> zap true
         val fixes =
           [] |> Term.add_free_names (Thm.prop_of zapped_th)
              |> filter is_zapped_var_name
         val ctxt' = ctxt |> Variable.add_fixes_direct fixes

                               String.isPrefix new_skolem_var_prefix s
                             | _ => false) fully_skolemized_t then
           let
             val (fully_skolemized_ct, ctxt) =
               Variable.import_terms true [fully_skolemized_t] ctxt
-              |>> the_single |>> Thm.global_cterm_of thy
+              |>> the_single |>> Thm.cterm_of ctxt
           in
             (SOME (discharger_th, fully_skolemized_ct),
              (Thm.assume fully_skolemized_ct, ctxt))
           end
        else

        (if new_skolem orelse null choice_ths then []
         else map (old_skolem_theorem_of_def ctxt) (old_skolem_defs th))
        th ctxt
     val (cnf_ths, ctxt) = clausify nnf_th
     fun intr_imp ct th =
-      Thm.instantiate ([], map (apply2 (Thm.global_cterm_of thy))
+      Thm.instantiate ([], map (apply2 (Thm.cterm_of ctxt))
                                [(Var (("i", 0), @{typ nat}),
                                  HOLogic.mk_nat ax_no)])
                       (zero_var_indexes @{thm skolem_COMBK_D})
       RS Thm.implies_intr ct th
   in