diff -r 55a71dd13ca0 -r 73af47bc277c src/ZF/Datatype.thy
--- a/src/ZF/Datatype.thy	Thu Aug 07 20:33:28 2025 +0200
+++ b/src/ZF/Datatype.thy	Thu Aug 07 21:40:03 2025 +0200
@@ -104,8 +104,8 @@
      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)