src/HOL/Tools/Function/function_lib.ML

           if null is
           then mk (Const (neu, ty), foldr1 mk (map (nth xs) js))
           else if null js
             then mk (foldr1 mk (map (nth xs) is), Const (neu, ty))
             else mk (foldr1 mk (map (nth xs) is), foldr1 mk (map (nth xs) js)))))
-     (K (rewrite_goals_tac ctxt ac
-         THEN resolve_tac ctxt [Drule.reflexive_thm] 1))
+     (fn {context = goal_ctxt, ...} =>
+       rewrite_goals_tac goal_ctxt ac THEN resolve_tac goal_ctxt [Drule.reflexive_thm] 1)
  end
 
 (* instance for unions *)
 fun regroup_union_conv ctxt =
   regroup_conv ctxt \<^const_abbrev>\<open>Set.empty\<close> \<^const_name>\<open>Lattices.sup\<close>