diff -r e84d900cd287 -r 59203adfc33f src/ZF/Datatype_ZF.thy
--- a/src/ZF/Datatype_ZF.thy	Thu Oct 30 16:20:46 2014 +0100
+++ b/src/ZF/Datatype_ZF.thy	Thu Oct 30 16:55:29 2014 +0100
@@ -95,7 +95,7 @@
          else ();
        val goal = Logic.mk_equals (old, new)
        val thm = Goal.prove ctxt [] [] goal
-         (fn _ => rtac @{thm iff_reflection} 1 THEN
+         (fn _ => resolve_tac @{thms iff_reflection} 1 THEN
            simp_tac (put_simpset datatype_ss ctxt addsimps #free_iffs lcon_info) 1)
          handle ERROR msg =>
          (warning (msg ^ "\ndata_free simproc:\nfailed to prove " ^ Syntax.string_of_term ctxt goal);