# HG changeset patch
# User desharna
# Date 1410522651 -7200
# Node ID a147bd03cad0ac563205a5232e29a13e675602cb
# Parent  7e142efcee1aa122bf0fdab79ce243b7e35a389e
make 'ctr_transfer' tactic more robust

diff -r 7e142efcee1a -r a147bd03cad0 src/HOL/Datatype_Examples/Misc_Datatype.thy
--- a/src/HOL/Datatype_Examples/Misc_Datatype.thy	Fri Sep 12 13:48:15 2014 +0200
+++ b/src/HOL/Datatype_Examples/Misc_Datatype.thy	Fri Sep 12 13:50:51 2014 +0200
@@ -153,6 +153,8 @@
 datatype (discs_sels) 'a dead_foo = A
 datatype (discs_sels) ('a, 'b) use_dead_foo = Y "'a" "'b dead_foo"
 
+datatype ('t, 'id) dead_sum_fun = Dead_sum_fun "('t list \<Rightarrow> 't) + 't" | Bar (bar: 'id)
+
 datatype (discs_sels) d1 = D
 datatype (discs_sels) d1' = is_D: D
 
diff -r 7e142efcee1a -r a147bd03cad0 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Fri Sep 12 13:48:15 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Fri Sep 12 13:50:51 2014 +0200
@@ -1591,7 +1591,8 @@
               val ctr_transfer_thms =
                 let val goals = map2 (mk_parametricity_goal names_lthy Rs) ctrAs ctrBs in
                   Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals)
-                    (K (mk_ctr_transfer_tac rel_intro_thms))
+                    (fn {context = ctxt, prems = _} =>
+                      mk_ctr_transfer_tac ctxt rel_intro_thms (map rel_eq_of_bnf live_nesting_bnfs))
                   |> Conjunction.elim_balanced (length goals)
                   |> Proof_Context.export names_lthy lthy
                   |> map Thm.close_derivation
diff -r 7e142efcee1a -r a147bd03cad0 src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Fri Sep 12 13:48:15 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Fri Sep 12 13:50:51 2014 +0200
@@ -21,7 +21,7 @@
   val mk_corec_disc_iff_tac: thm list -> thm list -> thm list -> Proof.context -> tactic
   val mk_ctor_iff_dtor_tac: Proof.context -> ctyp option list -> cterm -> cterm -> thm -> thm ->
     tactic
-  val mk_ctr_transfer_tac: thm list -> tactic
+  val mk_ctr_transfer_tac: Proof.context -> thm list -> thm list -> tactic
   val mk_disc_transfer_tac: thm -> thm -> thm list -> tactic
   val mk_exhaust_tac: Proof.context -> int -> thm list -> thm -> thm -> tactic
   val mk_half_distinct_tac: Proof.context -> thm -> thm -> thm list -> tactic
@@ -99,10 +99,11 @@
     ALLGOALS (REPEAT_ALL_NEW (atac ORELSE' rtac refl ORELSE' dtac @{thm rel_funD}))
   end;
 
-fun mk_ctr_transfer_tac rel_intros =
+fun mk_ctr_transfer_tac ctxt rel_intros rel_eqs =
   HEADGOAL Goal.conjunction_tac THEN
   ALLGOALS (REPEAT o (resolve_tac (@{thm rel_funI} :: rel_intros) THEN'
-    REPEAT_DETERM o atac));
+    TRY o (REPEAT_DETERM1 o atac ORELSE'
+      K (unfold_thms_tac ctxt rel_eqs) THEN' hyp_subst_tac ctxt THEN' rtac refl)));
 
 fun mk_disc_transfer_tac rel_sel exhaust_disc distinct_disc=
   let