src/HOL/Tools/Function/function_lib.ML

           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 rtac Drule.reflexive_thm 1))
+         THEN resolve_tac [Drule.reflexive_thm] 1))
  end
 
 (* instance for unions *)
 val regroup_union_conv =
   regroup_conv @{const_abbrev Set.empty} @{const_name Lattices.sup}