src/HOL/Tools/res_axioms.ML

       val newhyps = filter_out (member (op aconv) hyps0 o Thm.term_of) hyps
       val defs = filter (is_absko o Thm.term_of) newhyps
       val remaining_hyps = filter_out (member (op aconv) (map Thm.term_of defs))
                                       (map Thm.term_of hyps)
       val fixed = OldTerm.term_frees (concl_of st) @
-                  List.foldl (gen_union (op aconv)) [] (map OldTerm.term_frees remaining_hyps)
+                  List.foldl (union (op aconv)) [] (map OldTerm.term_frees remaining_hyps)
   in Seq.of_list [LocalDefs.expand (filter (is_okdef fixed o Thm.term_of) defs) st] end;
 
 
 fun meson_general_tac ctxt ths i st0 =
   let