--- 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
--- 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
--- 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