# HG changeset patch
# User traytel
# Date 1513496579 -3600
# Node ID 19809bc9d7ffcd5b5b09ae747219ed48285782d9
# Parent  62a5fbdded50d03a07bf74937a01a55f42e342c8
made tactics more robust

diff -r 62a5fbdded50 -r 19809bc9d7ff src/HOL/Tools/BNF/bnf_def.ML
--- 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;
diff -r 62a5fbdded50 -r 19809bc9d7ff src/HOL/Tools/BNF/bnf_def_tactics.ML
--- 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 =