src/HOL/Tools/BNF/bnf_def_tactics.ML
changeset 67222 19809bc9d7ff
parent 63714 b62f4f765353
child 67223 711eec20aecd
     1.1 --- a/src/HOL/Tools/BNF/bnf_def_tactics.ML	Sat Dec 16 22:32:04 2017 +0100
     1.2 +++ b/src/HOL/Tools/BNF/bnf_def_tactics.ML	Sun Dec 17 08:42:59 2017 +0100
     1.3 @@ -259,8 +259,11 @@
     1.4      (HEADGOAL (hyp_subst_tac ctxt THEN' rtac ctxt refl) ORELSE
     1.5       REPEAT_DETERM (HEADGOAL (eresolve_tac ctxt (Tactic.make_elim (in_rel RS iffD1) ::
     1.6         @{thms exE conjE CollectE}))) THEN
     1.7 -     HEADGOAL (hyp_subst_tac ctxt) THEN unfold_thms_tac ctxt rel_map THEN HEADGOAL (rtac ctxt iffI) THEN
     1.8 -     last_tac iffD1 THEN last_tac iffD2)
     1.9 +     HEADGOAL (hyp_subst_tac ctxt) THEN
    1.10 +     REPEAT_DETERM (HEADGOAL (resolve_tac ctxt (maps (fn thm =>
    1.11 +       [thm RS trans, thm RS @{thm trans[rotated, OF sym]}]) rel_map))) THEN
    1.12 +     HEADGOAL (rtac ctxt iffI) THEN
    1.13 +     last_tac iffD1 THEN  print_tac ctxt "baz" THEN last_tac iffD2)
    1.14    end;
    1.15  
    1.16  fun mk_map_transfer_tac ctxt rel_mono in_rel set_maps map_cong0 map_comp =