diff -r a3793600cb93 -r 4d3527b94f2a src/HOL/Tools/BNF/bnf_gfp_tactics.ML
--- 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))) =>