--- a/src/HOL/Tools/BNF/bnf_def.ML Sat Dec 16 22:32:04 2017 +0100
+++ b/src/HOL/Tools/BNF/bnf_def.ML Sun Dec 17 08:42:59 2017 +0100
@@ -1904,7 +1904,8 @@
Goal.prove_sorry lthy vars [] goal
(fn {context = ctxt, prems = _} =>
HEADGOAL (rtac ctxt (pred_set RSN (2, pred_set RSN (2, box_equals)))) THEN
- unfold_thms_tac ctxt (@{thm Ball_image_comp} :: map Lazy.force set_map) THEN
+ unfold_thms_tac ctxt
+ (@{thms Ball_image_comp ball_empty} @ map Lazy.force set_map) THEN
HEADGOAL (rtac ctxt refl))
|> Thm.close_derivation
end;
--- a/src/HOL/Tools/BNF/bnf_def_tactics.ML Sat Dec 16 22:32:04 2017 +0100
+++ b/src/HOL/Tools/BNF/bnf_def_tactics.ML Sun Dec 17 08:42:59 2017 +0100
@@ -259,8 +259,11 @@
(HEADGOAL (hyp_subst_tac ctxt THEN' rtac ctxt refl) ORELSE
REPEAT_DETERM (HEADGOAL (eresolve_tac ctxt (Tactic.make_elim (in_rel RS iffD1) ::
@{thms exE conjE CollectE}))) THEN
- HEADGOAL (hyp_subst_tac ctxt) THEN unfold_thms_tac ctxt rel_map THEN HEADGOAL (rtac ctxt iffI) THEN
- last_tac iffD1 THEN last_tac iffD2)
+ HEADGOAL (hyp_subst_tac ctxt) THEN
+ REPEAT_DETERM (HEADGOAL (resolve_tac ctxt (maps (fn thm =>
+ [thm RS trans, thm RS @{thm trans[rotated, OF sym]}]) rel_map))) THEN
+ HEADGOAL (rtac ctxt iffI) THEN
+ last_tac iffD1 THEN print_tac ctxt "baz" THEN last_tac iffD2)
end;
fun mk_map_transfer_tac ctxt rel_mono in_rel set_maps map_cong0 map_comp =