--- a/src/HOL/Tools/BNF/bnf_gfp_tactics.ML Sat Dec 12 15:37:42 2015 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_tactics.ML Sun Dec 13 21:56:15 2015 +0100
@@ -1082,7 +1082,7 @@
fun mk_rel_coinduct_tac ctxt CIHs in_rels in_Jrels helper_indss helper_coind1s helper_coind2s =
let val n = length in_rels;
in
- Method.insert_tac CIHs 1 THEN
+ Method.insert_tac ctxt CIHs 1 THEN
unfold_thms_tac ctxt (@{thm choice_iff} :: @{thm ex_simps(6)[symmetric]} :: in_rels) THEN
REPEAT_DETERM (etac ctxt exE 1) THEN
CONJ_WRAP' (fn (in_Jrel, (helper_inds, (helper_coind1, helper_coind2))) =>