src/HOL/Tools/Meson/meson_clausify.ML

       handle CTERM _ => (ct0, rev vars);
 
 (* 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 thy rhs0 =
-  let
-    val ctxt = Proof_Context.init_global thy  (* FIXME proper context!? *)
-
+fun old_skolem_theorem_of_def ctxt rhs0 =
+  let
+    val thy = Proof_Context.theory_of ctxt
     val rhs = rhs0 |> Type.legacy_freeze_thaw |> #1 |> cterm_of thy
     val rhs' = rhs |> Thm.dest_comb |> snd
     val (ch, frees) = c_variant_abs_multi (rhs', [])
     val (hilbert, cabs) = ch |> Thm.dest_comb |>> term_of
     val T =
       case hilbert of
         Const (_, Type (@{type_name fun}, [_, T])) => T
-      | _ => raise TERM ("old_skolem_theorem_of_def: expected \"Eps\"",
-                         [hilbert])
+      | _ => raise TERM ("old_skolem_theorem_of_def: expected \"Eps\"", [hilbert])
     val cex = cterm_of thy (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

     val choice_ths = choice_theorems thy
     val (opt, (nnf_th, ctxt)) =
       nnf_axiom choice_ths new_skolem ax_no th ctxt0
     fun clausify th =
       make_cnf (if new_skolem orelse null choice_ths then []
-                else map (old_skolem_theorem_of_def thy) (old_skolem_defs th))
+                else map (old_skolem_theorem_of_def ctxt) (old_skolem_defs th))
                th ctxt ctxt
     val (cnf_ths, ctxt) = clausify nnf_th
     fun intr_imp ct th =
       Thm.instantiate ([], map (pairself (cterm_of thy))
                                [(Var (("i", 0), @{typ nat}),