# HG changeset patch
# User desharna
# Date 1415705437 -3600
# Node ID d09bbd2642e294806e7e3595679b3687618c09e1
# Parent  6b6032e99a4bb4981ca8350b475bca9206b74e07
make 'corec_transfer' tactic more robust

diff -r 6b6032e99a4b -r d09bbd2642e2 src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Tue Nov 11 12:30:36 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Tue Nov 11 12:30:37 2014 +0100
@@ -251,10 +251,13 @@
     val num_pgs = length pgs;
     fun prem_no_of x = 1 + find_index (curry (op =) x) pgs;
 
-    val Inl_Inr_Pair_tac = REPEAT_DETERM o
-      (rtac (mk_rel_funDN 1 @{thm Inl_transfer}) ORELSE'
-       rtac (mk_rel_funDN 1 @{thm Inr_transfer}) ORELSE'
-       rtac (mk_rel_funDN 2 @{thm Pair_transfer}));
+    val Inl_Inr_Pair_tac = REPEAT_DETERM o (resolve_tac
+      [mk_rel_funDN 1 @{thm Inl_transfer},
+       mk_rel_funDN 1 @{thm Inl_transfer[of "op =" "op =", unfolded sum.rel_eq]},
+       mk_rel_funDN 1 @{thm Inr_transfer},
+       mk_rel_funDN 1 @{thm Inr_transfer[of "op =" "op =", unfolded sum.rel_eq]},
+       mk_rel_funDN 2 @{thm Pair_transfer},
+       mk_rel_funDN 2 @{thm Pair_transfer[of "op =" "op =", unfolded prod.rel_eq]}]);
 
     fun mk_unfold_If_tac total pos =
       HEADGOAL (Inl_Inr_Pair_tac THEN'