--- a/src/HOL/Tools/Metis/metis_tactic.ML Tue Dec 31 11:19:14 2013 +0100
+++ b/src/HOL/Tools/Metis/metis_tactic.ML Tue Dec 31 14:29:16 2013 +0100
@@ -64,7 +64,7 @@
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
@@ -101,7 +101,7 @@
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 =