src/HOL/Tools/BNF/bnf_fp_util.ML

     val phi = Proof_Context.export_morphism lthy_old lthy;
     val co_rec_names = map (fst o dest_Const o Morphism.term phi) co_rec_frees;
     val co_recs = @{map 2} (fn name => fn resT =>
       Const (name, co_rec_argTs ---> resT)) co_rec_names co_rec_resTs;
     val co_rec_defs = map (fn def =>
-      mk_unabs_def n (Morphism.thm phi def RS meta_eq_to_obj_eq)) co_rec_def_frees;
+      mk_unabs_def n (HOLogic.mk_obj_eq (Morphism.thm phi def))) co_rec_def_frees;
 
     val xtor_un_fold_xtor_thms =
       mk_xtor_un_fold_xtor_thms lthy fp (map (Term.subst_atomic_types (Xs ~~ Ts)) un_folds)
         xtors xtor_un_fold_unique map_id0s absT_info_opts;