src/ZF/Datatype_ZF.thy
changeset 58838 59203adfc33f
parent 54388 8b165615ffe3
child 58871 c399ae4b836f
     1.1 --- a/src/ZF/Datatype_ZF.thy	Thu Oct 30 16:20:46 2014 +0100
     1.2 +++ b/src/ZF/Datatype_ZF.thy	Thu Oct 30 16:55:29 2014 +0100
     1.3 @@ -95,7 +95,7 @@
     1.4           else ();
     1.5         val goal = Logic.mk_equals (old, new)
     1.6         val thm = Goal.prove ctxt [] [] goal
     1.7 -         (fn _ => rtac @{thm iff_reflection} 1 THEN
     1.8 +         (fn _ => resolve_tac @{thms iff_reflection} 1 THEN
     1.9             simp_tac (put_simpset datatype_ss ctxt addsimps #free_iffs lcon_info) 1)
    1.10           handle ERROR msg =>
    1.11           (warning (msg ^ "\ndata_free simproc:\nfailed to prove " ^ Syntax.string_of_term ctxt goal);