--- a/src/ZF/Datatype.thy Tue Aug 06 17:26:40 2019 +0200
+++ b/src/ZF/Datatype.thy Tue Aug 06 19:07:12 2019 +0200
@@ -97,7 +97,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 #free_iffs lcon_info) 1)
+ simp_tac (put_simpset datatype_ss ctxt addsimps
+ (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)