src/HOL/Tools/Function/function_context_tree.ML

               val assumes' = map (simplify (put_simpset HOL_basic_ss ctxt addsimps used)) assumes
 
               val (subeq, x') =
                 rewrite_help (fix @ fixes) (h_as @ assumes') x st
               val subeq_exp =
-                export_thm ctxt (fixes, assumes) (subeq RS meta_eq_to_obj_eq)
+                export_thm ctxt (fixes, assumes) (HOLogic.mk_obj_eq subeq)
             in
               (subeq_exp, x')
             end
           val (subthms, x') = fold_deps deps sub_step x
         in