--- a/src/HOL/Tools/BNF/bnf_fp_n2m_tactics.ML Thu Jul 16 10:48:20 2015 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_tactics.ML Thu Jul 16 12:23:22 2015 +0200
@@ -40,10 +40,10 @@
folded_C_IHs rel_monos unfolds;
in
unfold_thms_tac ctxt vimage2p_unfolds THEN
- HEADGOAL (CONJ_WRAP_GEN' (rtac @{thm context_conjI})
- (fn thm => rtac thm THEN_ALL_NEW (rotate_tac ~1 THEN'
+ HEADGOAL (CONJ_WRAP_GEN' (rtac ctxt @{thm context_conjI})
+ (fn thm => rtac ctxt thm THEN_ALL_NEW (rotate_tac ~1 THEN'
REPEAT_ALL_NEW (FIRST' [eresolve_tac ctxt C_IHs, eresolve_tac ctxt C_IH_monos,
- SELECT_GOAL (unfold_thms_tac ctxt nesting_rel_eqs) THEN' rtac @{thm order_refl},
+ SELECT_GOAL (unfold_thms_tac ctxt nesting_rel_eqs) THEN' rtac ctxt @{thm order_refl},
assume_tac ctxt, resolve_tac ctxt co_inducts,
resolve_tac ctxt C_IH_monos THEN' REPEAT_ALL_NEW (eresolve_tac ctxt nesting_rel_monos)])))
co_inducts)