src/HOL/Tools/BNF/bnf_fp_def_sugar.ML

         let val goals = map2 (mk_parametricity_goal names_lthy Rs) discAs discBs in
           if null goals then
             []
           else
             Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals)
-              (K (mk_disc_transfer_tac (the_single rel_sel_thms) (the_single exhaust_discs)
-                 (flat (flat distinct_discsss))))
+              (fn {context = ctxt, prems = _} => mk_disc_transfer_tac ctxt (the_single rel_sel_thms)
+                 (the_single exhaust_discs) (flat (flat distinct_discsss)))
             |> Conjunction.elim_balanced (length goals)
             |> Proof_Context.export names_lthy lthy
             |> map Thm.close_derivation
         end;