src/ZF/Datatype.thy

        if Config.get ctxt trace then tracing ("NEW = " ^ Syntax.string_of_term ctxt new)
        else ();
      val goal = Logic.mk_equals (old, new);
      val thm = Goal.prove ctxt [] [] goal
        (fn _ => resolve_tac ctxt @{thms iff_reflection} 1 THEN
-         simp_tac (put_simpset datatype_ss ctxt addsimps
-          (map (Thm.transfer thy) (#free_iffs lcon_info))) 1)
+         simp_tac (put_simpset datatype_ss ctxt
+          |> Simplifier.add_simps (map (Thm.transfer thy) (#free_iffs lcon_info))) 1)
        handle ERROR msg =>
        (warning (msg ^ "\ndata_free simproc:\nfailed to prove " ^ Syntax.string_of_term ctxt goal);
         raise Match)
   in SOME thm end
   handle Match => NONE;