src/CCL/CCL.thy

     let
       fun mk_inj_lemmas r = [@{thm arg_cong}] RL [r RS (r RS @{thm eq_lemma})]
       val inj_lemmas = maps mk_inj_lemmas rews
     in
       CHANGED (REPEAT (ares_tac [@{thm iffI}, @{thm allI}, @{thm conjI}] i ORELSE
-        eresolve_tac inj_lemmas i ORELSE
+        eresolve_tac ctxt inj_lemmas i ORELSE
         asm_simp_tac (ctxt addsimps rews) i))
     end;
 *}
 
 method_setup inj_rl = {*

 
 val ccl_dstncts =
   let
     fun mk_raw_dstnct_thm rls s =
       Goal.prove_global @{theory} [] [] (Syntax.read_prop_global @{theory} s)
-        (fn _ => rtac @{thm notI} 1 THEN eresolve_tac rls 1)
+        (fn {context = ctxt, ...} => rtac @{thm notI} 1 THEN eresolve_tac ctxt rls 1)
   in map (mk_raw_dstnct_thm caseB_lemmas)
     (mk_dstnct_rls @{theory} ["bot","true","false","pair","lambda"]) end
 
 fun mk_dstnct_thms ctxt defs inj_rls xs =
   let