src/HOL/Tools/Metis/metis_tactic.ML

   let
     val thy = Proof_Context.theory_of ctxt
     val tac = rewrite_goals_tac ctxt @{thms lambda_def [abs_def]} THEN rtac refl 1
     val t = hol_clause_of_metis ctxt type_enc sym_tab concealed mth
     val ct = cterm_of thy (HOLogic.mk_Trueprop t)
-  in Goal.prove_internal [] ct (K tac) |> Meson.make_meta_clause end
+  in Goal.prove_internal ctxt [] ct (K tac) |> Meson.make_meta_clause end
 
 fun add_vars_and_frees (t $ u) = fold (add_vars_and_frees) [t, u]
   | add_vars_and_frees (Abs (_, _, t)) = add_vars_and_frees t
   | add_vars_and_frees (t as Var _) = insert (op =) t
   | add_vars_and_frees (t as Free _) = insert (op =) t

       val eq_th = conv true ctxt (cprop_of th)
       (* We replace the equation's left-hand side with a beta-equivalent term
          so that "Thm.equal_elim" works below. *)
       val t0 $ _ $ t2 = prop_of eq_th
       val eq_ct = t0 $ prop_of th $ t2 |> cterm_of thy
-      val eq_th' = Goal.prove_internal [] eq_ct (K (rtac eq_th 1))
+      val eq_th' = Goal.prove_internal ctxt [] eq_ct (K (rtac eq_th 1))
     in Thm.equal_elim eq_th' th end
 
 fun clause_params ordering =
   {ordering = ordering,
    orderLiterals = Metis_Clause.UnsignedLiteralOrder,