src/ZF/Datatype.thy

          if !trace then writeln ("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 #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)
    in SOME thm end
    handle Match => NONE;